[inferbo] Rename forget_locs

Summary: The name was misleading, the function only forget locs for relations.

Reviewed By: ezgicicek

Differential Revision: D15045933

fbshipit-source-id: 7f41a55e7

infer/src/bufferoverrun/bufferOverrunAnalysis.ml

@@ -119,7 +119,7 @@ module TransferFunctions = struct
   let forget_ret_relation ret callee_pname mem =
     let ret_loc = Loc.of_pvar (Pvar.get_ret_pvar callee_pname) in
     let ret_var = Loc.of_var (Var.of_id (fst ret)) in
-    Dom.Mem.forget_locs (PowLoc.add ret_loc (PowLoc.singleton ret_var)) mem
+    Dom.Mem.relation_forget_locs (PowLoc.add ret_loc (PowLoc.singleton ret_var)) mem
 
 
   let is_external pname =
@@ -359,7 +359,7 @@ let compute_summary : local_decls -> CFG.t -> invariant_map -> memory_summary =
   let exit_node_id = CFG.exit_node cfg |> CFG.Node.id in
   match extract_post exit_node_id inv_map with
   | Some exit_mem ->
-      exit_mem |> Dom.Mem.forget_locs locals |> Dom.Mem.unset_oenv
+      exit_mem |> Dom.Mem.relation_forget_locs locals |> Dom.Mem.unset_oenv
   | None ->
       Bottom
 

infer/src/bufferoverrun/bufferOverrunChecker.ml

@@ -418,7 +418,7 @@ let get_checks_summary : BufferOverrunAnalysis.local_decls -> checks -> checks_s
        { cond_set
        ; unused_branches= _ (* intra-procedural *)
        ; unreachable_statements= _ (* intra-procedural *) } ->
-  PO.ConditionSet.for_summary ~forget_locs:locals cond_set
+  PO.ConditionSet.for_summary ~relation_forget_locs:locals cond_set
 
 
 let checker : Callbacks.proc_callback_args -> Summary.t =

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -1507,7 +1507,9 @@ module MemReach = struct
    fun locs symexp_opts -> lift_relation (Relation.store_relation locs symexp_opts)
 
 
-  let forget_locs : PowLoc.t -> t -> t = fun locs -> lift_relation (Relation.forget_locs locs)
+  let relation_forget_locs : PowLoc.t -> t -> t =
+   fun locs -> lift_relation (Relation.forget_locs locs)
+
 
   let init_param_relation : Loc.t -> t -> t = fun loc -> lift_relation (Relation.init_param loc)
 
@@ -1686,7 +1688,9 @@ module Mem = struct
    fun locs symexp_opts -> map ~f:(MemReach.store_relation locs symexp_opts)
 
 
-  let forget_locs : PowLoc.t -> t -> t = fun locs -> map ~f:(MemReach.forget_locs locs)
+  let relation_forget_locs : PowLoc.t -> t -> t =
+   fun locs -> map ~f:(MemReach.relation_forget_locs locs)
+
 
   let[@warning "-32"] init_param_relation : Loc.t -> t -> t =
    fun loc -> map ~f:(MemReach.init_param_relation loc)

infer/src/bufferoverrun/bufferOverrunProofObligations.ml

@@ -414,7 +414,7 @@ module ArrayAccessCondition = struct
         None
 
 
-  let forget_locs : AbsLoc.PowLoc.t -> t -> t =
+  let relation_forget_locs : AbsLoc.PowLoc.t -> t -> t =
    fun locs c -> {c with relation= Relation.forget_locs locs c.relation}
 end
 
@@ -693,10 +693,10 @@ module Condition = struct
         BinaryOperationCondition.check c trace
 
 
-  let forget_locs locs x =
+  let relation_forget_locs locs x =
     match x with
     | ArrayAccess c ->
-        ArrayAccess (ArrayAccessCondition.forget_locs locs c)
+        ArrayAccess (ArrayAccessCondition.relation_forget_locs locs c)
     | AllocSize _ | BinaryOperation _ ->
         x
 end
@@ -822,7 +822,7 @@ module ConditionWithTrace = struct
         report cwt.cond cwt.trace issue_type
 
 
-  let for_summary ~forget_locs = function
+  let for_summary ~relation_forget_locs = function
     | _, {propagate= false} | _, {report_issue_type= NotIssue} ->
         None
     | {cond; trace; reported; reachability}, {report_issue_type} ->
@@ -835,7 +835,7 @@ module ConditionWithTrace = struct
           | Issue issue_type ->
               Some (Reported.make issue_type)
         in
-        let cond = Condition.forget_locs forget_locs cond in
+        let cond = Condition.relation_forget_locs relation_forget_locs cond in
         let trace = ConditionTrace.for_summary trace in
         Some {cond; trace; reported; reachability}
 end
@@ -959,8 +959,8 @@ module ConditionSet = struct
     List.iter condset ~f:(ConditionWithTrace.report_errors ~report)
 
 
-  let for_summary ~forget_locs condset =
+  let for_summary ~relation_forget_locs condset =
-    List.filter_map condset ~f:(ConditionWithTrace.for_summary ~forget_locs)
+    List.filter_map condset ~f:(ConditionWithTrace.for_summary ~relation_forget_locs)
 
 
   let pp_summary : F.formatter -> _ t0 -> unit =

infer/src/bufferoverrun/bufferOverrunProofObligations.mli

@@ -84,7 +84,7 @@ module ConditionSet : sig
   val report_errors :
     report:(Condition.t -> ConditionTrace.t -> IssueType.t -> unit) -> checked_t -> unit
 
-  val for_summary : forget_locs:AbsLoc.PowLoc.t -> checked_t -> summary_t
+  val for_summary : relation_forget_locs:AbsLoc.PowLoc.t -> checked_t -> summary_t
 end
 
 val description : markup:bool -> Condition.t -> ConditionTrace.t -> string