From 672fd3a9a573a802444d8ae7e53e452e3624eebb Mon Sep 17 00:00:00 2001
From: Mehdi Bouaziz <mbouaziz@fb.com>
Date: Mon, 26 Mar 2018 05:49:45 -0700
Subject: [PATCH] [inferbo] Refactor 3/8: model_by_value without model_env

Reviewed By: jvillard

Differential Revision: D7397120

fbshipit-source-id: 1b8ac4e
---
 .../src/bufferoverrun/bufferOverrunChecker.ml | 33 +++++++++----------
 .../src/bufferoverrun/bufferOverrunModels.ml  |  7 ++--
 2 files changed, 21 insertions(+), 19 deletions(-)

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