[inferbo] Refactor 3/8: model_by_value without model_env

Reviewed By: jvillard

Differential Revision: D7397120

fbshipit-source-id: 1b8ac4e

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, _)
+      | Call (ret, Const Cfun callee_pname, params, location, _) -> (
-        -> (
+        match Models.Call.dispatch callee_pname params with
-          let model_env = Models.mk_model_env callee_pname node location tenv ?ret in
+        | Some {Models.exec} ->
-          match Models.Call.dispatch callee_pname params with
+            let model_env = Models.mk_model_env callee_pname node location tenv ?ret in
-          | Some {Models.exec} ->
+            exec model_env mem
-              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
+              L.(debug BufferOverrun Verbose)
-            | Some summary ->
+                "/!\\ Unknown call to %a at %a@\n" Typ.Procname.pp callee_pname Location.pp
-                let callee = extras callee_pname in
+                location ;
-                instantiate_mem tenv ret callee callee_pname params mem summary location
+              let val_unknown = Dom.Val.unknown_from ~callee_pname ~location in
-            | None ->
+              Models.model_by_value val_unknown ret 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 model_env 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 =

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