From 831741c5eb85e6317f7a03e648c8ebd40155e740 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Fri, 17 Jul 2020 08:56:11 -0700 Subject: [PATCH] [inferbo] Fix a bug in eval_arr Summary: This diff fixes a bug that eval_arr misses the case when a stack variable points to an array. Reviewed By: ezgicicek, roro47 Differential Revision: D22596999 fbshipit-source-id: 7c4a13d01 --- infer/src/bufferoverrun/bufferOverrunSemantics.ml | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml index 6a1caee84..aeb5c4ed5 100644 --- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml +++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml @@ -304,8 +304,11 @@ let rec eval_arr : Typ.IntegerWidths.t -> Exp.t -> Mem.t -> Val.t = fun integer_type_widths exp mem -> match exp with | Exp.Var id -> - let alias_loc = AliasTargets.find_simple_alias (Mem.find_alias_id id mem) in - Option.value_map alias_loc ~default:Val.bot ~f:(fun loc -> Mem.find loc mem) + let loc = + AliasTargets.find_simple_alias (Mem.find_alias_id id mem) + |> IOption.value_default_f ~f:(fun () -> Loc.of_id id) + in + Mem.find loc mem | Exp.Lvar pvar -> Mem.find (Loc.of_pvar pvar) mem | Exp.BinOp (bop, e1, e2) ->