diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index 4a221ddb5..86e1b22ab 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -49,10 +49,19 @@ struct = fun pname ret params node mem -> match ret with | Some (id, _) -> + let set_uninitialized typ loc mem = + match typ with + | Typ.Tint _ + | Typ.Tfloat _ -> + Dom.Mem.weak_update_heap loc Dom.Val.top_itv mem + | _ -> mem + in let (typ, size) = get_malloc_info (List.hd_exn params |> fst) in let size = Sem.eval size mem (CFG.loc node) |> Dom.Val.get_itv in let v = Sem.eval_array_alloc pname node typ Itv.zero size 0 1 in - Dom.Mem.add_stack (Loc.of_id id) v mem + mem + |> Dom.Mem.add_stack (Loc.of_id id) v + |> set_uninitialized typ (Dom.Val.get_array_locs v) | _ -> mem let model_realloc diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index 0e654d9ca..276f74c99 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -243,8 +243,11 @@ struct let get_array_blk : t -> ArrayBlk.astate = fun x -> x.arrayblk + let get_array_locs : t -> PowLoc.t + = fun x -> ArrayBlk.get_pow_loc x.arrayblk + let get_all_locs : t -> PowLoc.t - = fun x -> ArrayBlk.get_pow_loc x.arrayblk |> PowLoc.join x.powloc + = fun x -> PowLoc.join x.powloc (get_array_locs x) let top_itv : t = { bot with itv = Itv.top } diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index 6c4c966d0..269d8a953 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -8,4 +8,4 @@ codetoanalyze/c/bufferoverrun/goto_loop.c, goto_loop, 11, BUFFER_OVERRUN, [Offse codetoanalyze/c/bufferoverrun/nested_loop.c, nested_loop, 7, BUFFER_OVERRUN, [Offset : [0, 10] Size : [10, 10] @ codetoanalyze/c/bufferoverrun/nested_loop.c:20:7] codetoanalyze/c/bufferoverrun/nested_loop_with_label.c, nested_loop_with_label, 6, BUFFER_OVERRUN, [Offset : [0, +oo] Size : [10, 10] @ codetoanalyze/c/bufferoverrun/nested_loop_with_label.c:19:5] codetoanalyze/c/bufferoverrun/trivial.c, trivial, 2, BUFFER_OVERRUN, [Offset : [10, 10] Size : [10, 10] @ codetoanalyze/c/bufferoverrun/trivial.c:15:3] -codetoanalyze/c/bufferoverrun/while_loop.c, while_loop, 3, BUFFER_OVERRUN, [Offset : [0, +oo] Size : [10, 10] @ codetoanalyze/c/bufferoverrun/while_loop.c:18:10] +codetoanalyze/c/bufferoverrun/while_loop.c, while_loop, 3, BUFFER_OVERRUN, [Offset : [0, +oo] Size : [10, 10] @ codetoanalyze/c/bufferoverrun/while_loop.c:16:10] diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/while_loop.c b/infer/tests/codetoanalyze/c/bufferoverrun/while_loop.c index 6d8a9a080..40d9a41a2 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/while_loop.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/while_loop.c @@ -10,11 +10,9 @@ * of patent rights can be found in the PATENTS file in the same directory. */ -char* safealloc(int n); - void while_loop() { int i = 0; - char* a = safealloc(10); + char* a = malloc(10); while (*(a + i) && i < 10) /* BUG */ a[i++] = 1; /* SAFE */ }