[inferbo] Add some tests of imprecise pruning on unsigned int

Reviewed By: mbouaziz

Differential Revision: D10483516

fbshipit-source-id: 945ccb603

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

@@ -240,3 +240,55 @@ void mult_minimum_Bad() {
   int64_t x = -1;
   int64_t y = x * INT64_MIN;
 }
+
+void unsigned_prune_zero1_Good(unsigned int x) {
+  if (x != 0) {
+    unsigned int y = x - 1;
+  }
+}
+
+void call_unsigned_prune_zero1_Good_FP() { unsigned_prune_zero1_Good(0); }
+
+void unsigned_prune_zero2_Good(unsigned int y) {
+  unsigned int x = y;
+  for (; x; --x) {
+  }
+}
+
+void call_unsigned_prune_zero2_Good_FP() { unsigned_prune_zero2_Good(0); }
+
+void unsigned_prune_ge1_Good(unsigned int x, unsigned int y) {
+  if (x >= y) {
+    unsigned int z = x - y;
+  }
+}
+
+void call_unsigned_prune_ge1_Good_FP() { unsigned_prune_ge1_Good(0, 1); }
+
+void unsigned_prune_ge2_Good(unsigned int x, unsigned int y) {
+  if (y > 0) {
+    if (x >= y) {
+      unsigned int z = x - 1;
+    }
+  }
+}
+
+void call_unsigned_prune_ge2_Good_FP() { unsigned_prune_ge2_Good(0, 1); }
+
+void unsigned_prune_ge3_Good(unsigned int x, unsigned int y) {
+  if (y > 0) {
+    if (x >= y + 1) {
+      unsigned int z = x - 1;
+    }
+  }
+}
+
+void call_unsigned_prune_ge3_Good_FP() { unsigned_prune_ge3_Good(0, 1); }
+
+void unsigned_prune_gt(unsigned int x, unsigned int y) {
+  if (x > 0) {
+    unsigned int z = x - y;
+  }
+}
+
+void call_unsigned_prune_gt_Good_FP() { unsigned_prune_gt(0, 3); }

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

@@ -1,3 +1,9 @@
+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_ge2_Good_FP, 0, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,Parameter: x,Binop: (0 - 1):unsigned32 by call to `unsigned_prune_ge2_Good` ]
+codetoanalyze/c/bufferoverrun/arith.c, call_unsigned_prune_ge3_Good_FP, 0, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,Parameter: x,Binop: (0 - 1):unsigned32 by call to `unsigned_prune_ge3_Good` ]
+codetoanalyze/c/bufferoverrun/arith.c, call_unsigned_prune_gt_Good_FP, 0, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,Parameter: x,Binop: ([1, 0] - 3):unsigned32 by call to `unsigned_prune_gt` ]
+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, []
 codetoanalyze/c/bufferoverrun/arith.c, integer_overflow_by_addition_l2_Bad, 7, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [Assignment,Binop: ([0, 2000000000] + [0, 2000000000]):signed32]