[inferbo] Add a test showing limitation of min/max domain

Summary: Since Inferbo's current min/max domain can keep only a single symbol, e.g. min(constant, symbol) , it loses precision when trying to prune a value including multiple symbols.

Reviewed By: ezgicicek

Differential Revision: D14099399

fbshipit-source-id: 71d677b75

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

@@ -260,6 +260,7 @@ codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_or_Ok, 3, CONDITION_ALW
 codetoanalyze/c/bufferoverrun/prune_constant.c, call_fromHex2_200_Good_FP, 3, BUFFER_OVERRUN_L3, no_bucket, ERROR, [<Offset trace>,Call,Assignment,Assignment,<Length trace>,Array declaration,Array access: Offset: [-28, 16] Size: 17]
 codetoanalyze/c/bufferoverrun/prune_constant.c, call_fromHex2_sym_Good_FP, 3, BUFFER_OVERRUN_L3, no_bucket, ERROR, [<Offset trace>,Call,Assignment,Assignment,<Length trace>,Array declaration,Array access: Offset: [-28, 16] Size: 17]
 codetoanalyze/c/bufferoverrun/prune_constant.c, call_greater_than_Good_FP, 3, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [<LHS trace>,Assignment,Binary operation: (0 - 1):unsigned32]
+codetoanalyze/c/bufferoverrun/prune_constant.c, call_null_pruning_symbols_Good_FP, 0, BUFFER_OVERRUN_L3, no_bucket, ERROR, [Call,<Offset trace>,Parameter `a`,Assignment,<Length trace>,Parameter `a`,Assignment,Array declaration,Array access: Offset: [0, 29] Size: [1, 30] by call to `null_pruning_symbols` ]
 codetoanalyze/c/bufferoverrun/prune_constant.c, call_prune_add2_2_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,<Offset trace>,Parameter `x`,<Length trace>,Array declaration,Array access: Offset: 10 Size: 10 by call to `prune_add2` ]
 codetoanalyze/c/bufferoverrun/prune_constant.c, call_prune_sub2_2_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,<Offset trace>,Parameter `x`,<Length trace>,Array declaration,Array access: Offset: 10 Size: 10 by call to `prune_sub2` ]
 codetoanalyze/c/bufferoverrun/prune_constant.c, null_pruning1_Bad, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]

infer/tests/codetoanalyze/c/bufferoverrun/prune_constant.c

@@ -173,3 +173,13 @@ void call_greater_than_Good_FP() {
     idx = idx - 1;
   }
 }
+
+void null_pruning_symbols(unsigned int a, unsigned int b) {
+  unsigned int c = a + b;
+  if (c > 0) {
+    char result[c];
+    result[c - 1] = 0;
+  }
+}
+
+void call_null_pruning_symbols_Good_FP() { null_pruning_symbols(10, 20); }