From 5260558fef21944fe764b3036cc240e7b89c7edf Mon Sep 17 00:00:00 2001 From: Mehdi Bouaziz Date: Tue, 10 Apr 2018 09:53:34 -0700 Subject: [PATCH] [inferbo][easy] Simplify mk_MinMax Reviewed By: jvillard Differential Revision: D7556208 fbshipit-source-id: cc667fb --- infer/src/bufferoverrun/itv.ml | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml index fb80c8147..372eb87b1 100644 --- a/infer/src/bufferoverrun/itv.ml +++ b/infer/src/bufferoverrun/itv.ml @@ -377,18 +377,16 @@ module Bound = struct let is_mone_symbol : t -> bool = fun x -> get_mone_symbol_opt x <> None let mk_MinMax (c, sign, m, d, s) = - if Symbol.is_unsigned s then + if Symbol.is_unsigned s && d <= 0 then match m with - | Min when d <= 0 -> + | Min -> of_int (Sign.eval_int sign c d) - | Max when d <= 0 -> ( + | Max -> match sign with | Plus -> Linear (c, SymLinear.singleton_one s) | Minus -> - Linear (c, SymLinear.singleton_minus_one s) ) - | _ -> - MinMax (c, sign, m, d, s) + Linear (c, SymLinear.singleton_minus_one s) else MinMax (c, sign, m, d, s)