[inferbo] Add traces on cast

Reviewed By: mbouaziz

Differential Revision: D13606790

fbshipit-source-id: a3d6d0c5c

infer/src/bufferoverrun/bufferOverrunSemantics.ml

@@ -163,7 +163,7 @@ let rec eval : Typ.IntegerWidths.t -> Exp.t -> Mem.t -> Val.t =
           (* We treat "(unsigned int)-1" case specially, because programmers often exploit it to get
              the max number of the type. *)
           let ikind = Option.value_exn (Typ.get_ikind_opt t) in
-          Val.of_itv (Itv.max_of_ikind integer_type_widths ikind)
+          Val.of_itv ~traces:(Val.get_traces v) (Itv.max_of_ikind integer_type_widths ikind)
         else v
     | Exp.Lfield (e, fn, _) ->
         let v = eval integer_type_widths e mem in

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

@@ -77,7 +77,7 @@ codetoanalyze/c/bufferoverrun/cast.c, cast_float_to_int_Bad_FN, 4, CONDITION_ALW
 codetoanalyze/c/bufferoverrun/cast.c, cast_float_to_int_Good, 4, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
 codetoanalyze/c/bufferoverrun/cast.c, cast_signed_to_unsigned2_Bad_FN, 4, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
 codetoanalyze/c/bufferoverrun/cast.c, cast_signed_to_unsigned_Bad, 4, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
-codetoanalyze/c/bufferoverrun/cast.c, cast_signed_to_unsigned_Bad, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: 4294967295 Size: 10]
+codetoanalyze/c/bufferoverrun/cast.c, cast_signed_to_unsigned_Bad, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,Assignment,<Length trace>,Array declaration,Array access: Offset: 4294967295 Size: 10]
 codetoanalyze/c/bufferoverrun/cast.c, cast_signed_to_unsigned_Good, 4, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
 codetoanalyze/c/bufferoverrun/cast.c, cast_unsigned_to_signed_Bad_FN, 4, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
 codetoanalyze/c/bufferoverrun/cast.c, cast_unsigned_to_signed_Good, 4, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]