diff --git a/infer/src/IR/HilInstr.ml b/infer/src/IR/HilInstr.ml index bf348f0e2..d27f831a0 100644 --- a/infer/src/IR/HilInstr.ml +++ b/infer/src/IR/HilInstr.ml @@ -22,7 +22,7 @@ type t = | Assign of HilExp.AccessExpression.t * HilExp.t * Location.t | Assume of HilExp.t * [`Then | `Else] * Sil.if_kind * Location.t | Call of AccessPath.base * call * HilExp.t list * CallFlags.t * Location.t - | ExitScope of Var.t list + | ExitScope of Var.t list * Location.t [@@deriving compare] let pp fmt = function @@ -35,8 +35,8 @@ let pp fmt = function let pp_ret fmt = F.fprintf fmt "%a := " AccessPath.pp_base in let pp_actuals fmt = PrettyPrintable.pp_collection ~pp_item:HilExp.pp fmt in F.fprintf fmt "%a%a(%a) [%a]" pp_ret ret pp_call call pp_actuals actuals Location.pp loc - | ExitScope vars -> - F.fprintf fmt "exit scope [%a]" (Pp.seq ~sep:"; " Var.pp) vars + | ExitScope (vars, loc) -> + F.fprintf fmt "exit scope(%a) [%a]" (Pp.seq ~sep:"; " Var.pp) vars Location.pp loc type translation = Instr of t | Bind of Var.t * HilExp.AccessExpression.t | Ignore @@ -121,8 +121,8 @@ let of_sil ~include_array_indexes ~f_resolve_id (instr : Sil.instr) = let hil_exp = exp_of_sil exp (Typ.mk (Tint IBool)) in let branch = if true_branch then `Then else `Else in Instr (Assume (hil_exp, branch, if_kind, loc)) - | ExitScope (vars, _) -> - Instr (ExitScope vars) + | ExitScope (vars, loc) -> + Instr (ExitScope (vars, loc)) | Abstract _ | Nullify _ -> (* these don't seem useful for most analyses. can translate them later if we want to *) Ignore diff --git a/infer/src/IR/HilInstr.mli b/infer/src/IR/HilInstr.mli index cdc86a8c5..83950555d 100644 --- a/infer/src/IR/HilInstr.mli +++ b/infer/src/IR/HilInstr.mli @@ -18,7 +18,7 @@ type t = (** Assumed expression, true_branch boolean, source of the assume (conditional, ternary, etc.) *) | Call of AccessPath.base * call * HilExp.t list * CallFlags.t * Location.t (** Var to hold the return, call expression, formals *) - | ExitScope of Var.t list + | ExitScope of Var.t list * Location.t [@@deriving compare] val pp : F.formatter -> t -> unit diff --git a/infer/src/absint/LowerHil.ml b/infer/src/absint/LowerHil.ml index 27466f63f..a924e2134 100644 --- a/infer/src/absint/LowerHil.ml +++ b/infer/src/absint/LowerHil.ml @@ -72,13 +72,13 @@ module Make (TransferFunctions : TransferFunctions.HIL) (HilConfig : HilConfig) (None, bindings) | Bind (id, access_path) -> (None, Bindings.add id access_path bindings) - | Instr (ExitScope vars) -> + | Instr (ExitScope (vars, loc)) -> let bindings, vars = List.fold vars ~init:(bindings, []) ~f:(fun (bindings, vars) var -> let bindings, vars' = Bindings.exit_scope var bindings in (bindings, append_bindings vars vars') ) in - let instr = if List.is_empty vars then None else Some (HilInstr.ExitScope vars) in + let instr = if List.is_empty vars then None else Some (HilInstr.ExitScope (vars, loc)) in (instr, bindings) | Instr instr -> (Some instr, bindings) diff --git a/infer/src/checkers/Pulse.ml b/infer/src/checkers/Pulse.ml index 0359d6492..379f94855 100644 --- a/infer/src/checkers/Pulse.ml +++ b/infer/src/checkers/Pulse.ml @@ -136,7 +136,7 @@ module PulseTransferFunctions (CFG : ProcCfg.S) = struct PulseDomain.read_all loc (HilExp.get_access_exprs condition) astate |> check_error summary | Call (ret, call, actuals, flags, loc) -> dispatch_call summary ret call actuals flags loc astate |> check_error summary - | ExitScope vars -> + | ExitScope (vars, _) -> PulseDomain.remove_vars vars astate