[inferbo] Move get_formals

Reviewed By: jvillard

Differential Revision: D13294600

fbshipit-source-id: acd67487a

infer/src/bufferoverrun/bufferOverrunChecker.ml

@@ -172,7 +172,7 @@ module Init = struct
     in
     let mem = Dom.Mem.init in
     let mem, _ = List.fold ~f:try_decl_local ~init:(mem, 1) (Procdesc.get_locals pdesc) in
-    let formals = Sem.get_formals pdesc in
+    let formals = Dom.get_formals pdesc in
     declare_symbolic_parameters pname tenv integer_type_widths ~node_hash location symbol_table
       formals mem
 end
@@ -216,7 +216,7 @@ module TransferFunctions = struct
     let ret_var = Loc.of_var (Var.of_id ret_id) in
     let ret_val = Dom.Mem.find (Loc.of_pvar (Pvar.get_ret_pvar callee_pname)) callee_exit_mem in
     let formals =
-      List.fold (Sem.get_formals callee_pdesc) ~init:PowLoc.bot ~f:(fun acc (formal, _) ->
+      List.fold (Dom.get_formals callee_pdesc) ~init:PowLoc.bot ~f:(fun acc (formal, _) ->
           let v = Dom.Mem.find (Loc.of_pvar formal) callee_exit_mem in
           PowLoc.join acc (Dom.Val.get_all_locs v) )
     in
@@ -308,7 +308,7 @@ module TransferFunctions = struct
                 let pname = Procdesc.get_proc_name pdesc in
                 match Typ.Procname.get_method pname with
                 | "__inferbo_empty" when Loc.is_return loc_v -> (
-                  match Sem.get_formals pdesc with
+                  match Dom.get_formals pdesc with
                   | [(formal, _)] ->
                       let formal_v = Dom.Mem.find (Loc.of_pvar formal) mem in
                       Dom.Mem.store_empty_alias formal_v loc_v mem

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -21,6 +21,12 @@ type eval_sym_trace =
   ; trace_of_sym: Symb.Symbol.t -> Trace.Set.t
   ; eval_locpath: PowLoc.eval_locpath }
 
+let get_formals : Procdesc.t -> (Pvar.t * Typ.t) list =
+ fun pdesc ->
+  let proc_name = Procdesc.get_proc_name pdesc in
+  Procdesc.get_formals pdesc |> List.map ~f:(fun (name, typ) -> (Pvar.mk name proc_name, typ))
+
+
 module Val = struct
   type t =
     { itv: Itv.t

infer/src/bufferoverrun/bufferOverrunSemantics.ml

@@ -296,12 +296,6 @@ let rec eval_arr : Typ.IntegerWidths.t -> Exp.t -> Mem.t -> Val.t =
       Val.bot
 
 
-let get_formals : Procdesc.t -> (Pvar.t * Typ.t) list =
- fun pdesc ->
-  let proc_name = Procdesc.get_proc_name pdesc in
-  Procdesc.get_formals pdesc |> List.map ~f:(fun (name, typ) -> (Pvar.mk name proc_name, typ))
-
-
 module ParamBindings = struct
   include PrettyPrintable.MakePPMap (struct
     include Pvar

infer/src/checkers/reachingDefs.ml

@@ -59,7 +59,7 @@ end
 (* initialize formal parameters to have start node as reaching def *)
 let init_reaching_defs_with_formals pdesc =
   let start_node_defs = Defs.singleton (Procdesc.get_start_node pdesc) in
-  BufferOverrunSemantics.get_formals pdesc
+  BufferOverrunDomain.get_formals pdesc
   |> List.fold_left ~init:ReachingDefsMap.empty ~f:(fun acc (pvar, _) ->
          ReachingDefsMap.add (Var.of_pvar pvar) start_node_defs acc )