diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index 5a27c1c4c..5b6843862 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -246,24 +246,23 @@ module TransferFunctions (CFG : ProcCfg.S) = struct mem | Prune (exp, _, _, _) -> Sem.prune exp mem - | Call (ret, Const Cfun callee_pname, params, location, _) - -> ( - let model_env = Models.mk_model_env callee_pname node location tenv ?ret in - match Models.Call.dispatch callee_pname params with - | Some {Models.exec} -> - exec model_env mem + | Call (ret, Const Cfun callee_pname, params, location, _) -> ( + match Models.Call.dispatch callee_pname params with + | Some {Models.exec} -> + let model_env = Models.mk_model_env callee_pname node location tenv ?ret in + exec model_env mem + | None -> + match Summary.read_summary pdesc callee_pname with + | Some summary -> + let callee = extras callee_pname in + instantiate_mem tenv ret callee callee_pname params mem summary location | None -> - match Summary.read_summary pdesc callee_pname with - | Some summary -> - let callee = extras callee_pname in - instantiate_mem tenv ret callee callee_pname params mem summary location - | None -> - L.(debug BufferOverrun Verbose) - "/!\\ Unknown call to %a at %a@\n" Typ.Procname.pp callee_pname Location.pp - location ; - let val_unknown = Dom.Val.unknown_from ~callee_pname ~location in - Models.model_by_value val_unknown model_env mem - |> Dom.Mem.add_heap Loc.unknown val_unknown ) + L.(debug BufferOverrun Verbose) + "/!\\ Unknown call to %a at %a@\n" Typ.Procname.pp callee_pname Location.pp + location ; + let val_unknown = Dom.Val.unknown_from ~callee_pname ~location in + Models.model_by_value val_unknown ret mem |> Dom.Mem.add_heap Loc.unknown val_unknown + ) | Declare_locals (locals, location) -> (* array allocation in stack e.g., int arr[10] *) let rec decl_local pname node location loc typ ~inst_num ~dimension mem = diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index 7cbb5a060..95e7124db 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -167,7 +167,7 @@ module Make (BoUtils : BufferOverrunUtils.S) = struct {exec; check} - let model_by_value value {ret} mem = + let model_by_value value ret mem = match ret with | Some (id, _) -> Dom.Mem.add_stack (Loc.of_id id) value mem @@ -177,7 +177,10 @@ module Make (BoUtils : BufferOverrunUtils.S) = struct mem - let by_value value = {exec= model_by_value value; check= no_check} + let by_value value = + let exec {ret} mem = model_by_value value ret mem in + {exec; check= no_check} + let bottom = let exec _model_env _mem = Bottom in