[inferbo] Ignore __variable_initialization

Summary: Avoid introducing unknown values by __variable_initialization.

Reviewed By: mbouaziz

Differential Revision: D13254059

fbshipit-source-id: 75751fa70

infer/src/bufferoverrun/bufferOverrunModels.ml

@@ -56,6 +56,8 @@ type declare_symbolic_fun =
 
 type typ_model = {declare_local: declare_local_fun; declare_symbolic: declare_symbolic_fun}
 
+let no_exec _model_env ~ret:_ mem = mem
+
 let no_check _model_env _mem cond_set = cond_set
 
 (* It returns a tuple of:
@@ -212,6 +214,8 @@ let inferbo_set_size e1 e2 =
 
 let model_by_value value (id, _) mem = Dom.Mem.add_stack (Loc.of_id id) value mem
 
+let nop = {exec= no_exec; check= no_check}
+
 let by_value =
   let exec ~value _ ~ret mem = model_by_value value ret mem in
   fun value -> {exec= exec ~value; check= no_check}
@@ -499,6 +503,7 @@ module Call = struct
     make_dispatcher
       [ -"__inferbo_min" <>$ capt_exp $+ capt_exp $!--> inferbo_min
       ; -"__inferbo_set_size" <>$ capt_exp $+ capt_exp $!--> inferbo_set_size
+      ; -"__variable_initialization" <>--> nop
       ; -"__exit" <>--> bottom
       ; -"exit" <>--> bottom
       ; -"fgetc" <>--> by_value Dom.Val.Itv.m1_255

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

@@ -3,9 +3,9 @@ codetoanalyze/c/bufferoverrun/arith.c, band_negative_Bad, 8, BUFFER_OVERRUN_L2,
 codetoanalyze/c/bufferoverrun/arith.c, band_negative_constant_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: 1 Size: 1]
 codetoanalyze/c/bufferoverrun/arith.c, band_positive_Bad, 6, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Call,Assignment,Assignment,Assignment,<Length trace>,Array declaration,Array access: Offset: [0, 8] Size: 5]
 codetoanalyze/c/bufferoverrun/arith.c, band_positive_constant_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: 2 Size: 2]
-codetoanalyze/c/bufferoverrun/arith.c, call_scan_hex_Good_FP, 2, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [Unknown value from: __variable_initialization,Call,<LHS trace>,Parameter `*cp`,Assignment,Binary operation: ([58, +oo] - 97):unsigned64 by call to `scan_hex_Good` ]
-codetoanalyze/c/bufferoverrun/arith.c, call_scan_hex_Good_FP, 2, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [Unknown value from: __variable_initialization,Call,<LHS trace>,Parameter `*cp`,Assignment,Binary operation: ([58, 102] - 87):unsigned64 by call to `scan_hex_Good` ]
-codetoanalyze/c/bufferoverrun/arith.c, call_scan_hex_Good_FP, 2, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [Unknown value from: __variable_initialization,Call,<LHS trace>,Parameter `*cp`,Assignment,Binary operation: ([-oo, +oo] - 48):unsigned64 by call to `scan_hex_Good` ]
+codetoanalyze/c/bufferoverrun/arith.c, call_scan_hex_Good_FP, 2, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [Call,<LHS trace>,Parameter `*cp`,Assignment,Binary operation: ([58, +oo] - 97):unsigned64 by call to `scan_hex_Good` ]
+codetoanalyze/c/bufferoverrun/arith.c, call_scan_hex_Good_FP, 2, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [Call,<LHS trace>,Parameter `*cp`,Assignment,Binary operation: ([58, 102] - 87):unsigned64 by call to `scan_hex_Good` ]
+codetoanalyze/c/bufferoverrun/arith.c, call_scan_hex_Good_FP, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,<LHS trace>,Parameter `*cp`,Assignment,Binary operation: ([-oo, +oo] - 48):unsigned64 by call to `scan_hex_Good` ]
 codetoanalyze/c/bufferoverrun/arith.c, call_two_safety_conditions2_Bad, 1, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,<LHS trace>,Call,Assignment,Assignment,<RHS trace>,Parameter `s`,Binary operation: ([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,<LHS trace>,Parameter `x`,<RHS trace>,Parameter `y`,Binary operation: (0 - 1):unsigned32 by call to `unsigned_prune_ge1_Good` ]
 codetoanalyze/c/bufferoverrun/arith.c, div_const2_FP, 3, BUFFER_OVERRUN_L5, no_bucket, ERROR, [<Offset trace>,Parameter `n`,Assignment,<Length trace>,Array declaration,Array access: Offset: [-oo, +oo] Size: 1]