From 68d0fa8f44bae8c2cc29d7ea003b3b9f78918619 Mon Sep 17 00:00:00 2001 From: Mehdi Bouaziz Date: Wed, 24 Apr 2019 03:58:46 -0700 Subject: [PATCH] [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 | 4 ++-- infer/src/bufferoverrun/bufferOverrunChecker.ml | 2 +- infer/src/bufferoverrun/bufferOverrunDomain.ml | 8 ++++++-- .../bufferoverrun/bufferOverrunProofObligations.ml | 14 +++++++------- .../bufferOverrunProofObligations.mli | 2 +- 5 files changed, 17 insertions(+), 13 deletions(-) diff --git a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml index 4bac26566..99895ddd4 100644 --- a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml +++ b/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 diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index d25fae443..732c721f1 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/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 = diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index dba0543b0..d07554b6c 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/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) diff --git a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml index d606a523a..8ef38916a 100644 --- a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml +++ b/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 = - List.filter_map condset ~f:(ConditionWithTrace.for_summary ~forget_locs) + let for_summary ~relation_forget_locs condset = + List.filter_map condset ~f:(ConditionWithTrace.for_summary ~relation_forget_locs) let pp_summary : F.formatter -> _ t0 -> unit = diff --git a/infer/src/bufferoverrun/bufferOverrunProofObligations.mli b/infer/src/bufferoverrun/bufferOverrunProofObligations.mli index 591bb577d..dde2bee08 100644 --- a/infer/src/bufferoverrun/bufferOverrunProofObligations.mli +++ b/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