[inferbo] Preciser pruning: (x != 0)

Reviewed By: mbouaziz

Differential Revision: D12898535

fbshipit-source-id: ec83c7308

infer/src/bufferoverrun/itv.ml

@@ -750,8 +750,8 @@ module ItvPure = struct
 
   let prune_diff : t -> Bound.t -> t bottom_lifted =
    fun ((l, u) as itv) b ->
-    if Bound.eq l b then normalize (Bound.plus_l l Bound.one, u)
-    else if Bound.eq u b then normalize (l, Bound.plus_u u Bound.mone)
+    if Bound.le b l then normalize (prune_gt itv (of_bound b))
+    else if Bound.le u b then normalize (prune_lt itv (of_bound b))
     else NonBottom itv
 
 

infer/tests/codetoanalyze/c/bufferoverrun/arith.c

@@ -247,7 +247,7 @@ void unsigned_prune_zero1_Good(unsigned int x) {
   }
 }
 
-void call_unsigned_prune_zero1_Good_FP() { unsigned_prune_zero1_Good(0); }
+void call_unsigned_prune_zero1_Good() { unsigned_prune_zero1_Good(0); }
 
 void unsigned_prune_zero2_Good(unsigned int y) {
   unsigned int x = y;

infer/tests/codetoanalyze/c/bufferoverrun/issues.exp

@@ -1,6 +1,5 @@
 codetoanalyze/c/bufferoverrun/arith.c, call_two_safety_conditions2_Bad, 1, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Parameter: s,Binop: ([0, +oo] + 15):unsigned32 by call to `two_safety_conditions2_Bad` ]
 codetoanalyze/c/bufferoverrun/arith.c, call_unsigned_prune_ge1_Good_FP, 0, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,Parameter: x,Binop: (0 - 1):unsigned32 by call to `unsigned_prune_ge1_Good` ]
-codetoanalyze/c/bufferoverrun/arith.c, call_unsigned_prune_zero1_Good_FP, 0, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,Parameter: x,Binop: (0 - 1):unsigned32 by call to `unsigned_prune_zero1_Good` ]
 codetoanalyze/c/bufferoverrun/arith.c, call_unsigned_prune_zero2_Good_FP, 0, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,Parameter: y,Assignment,Binop: ([-oo, 0] - 1):unsigned32 by call to `unsigned_prune_zero2_Good` ]
 codetoanalyze/c/bufferoverrun/arith.c, integer_overflow_by_addition_Bad, 4, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Assignment,Binop: (2000000000 + 2000000000):signed32]
 codetoanalyze/c/bufferoverrun/arith.c, integer_overflow_by_addition_Bad, 5, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, []