diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml index dff7e96ca..55fcfa2c6 100644 --- a/infer/src/pulse/Pulse.ml +++ b/infer/src/pulse/Pulse.ml @@ -159,7 +159,7 @@ module PulseTransferFunctions = struct (* invalidate both [&x] and [x]: reading either is now forbidden *) let invalidate access_expr = PulseOperations.invalidate - (PulseTrace.Immediate {imm= GoneOutOfScope (access_expr, call_loc); location= call_loc}) + (PulseTrace.Immediate {imm= GoneOutOfScope access_expr; location= call_loc}) call_loc access_expr in invalidate (HilExp.AccessExpression.dereference out_of_scope_access_expr) astate diff --git a/infer/src/pulse/PulseInvalidation.ml b/infer/src/pulse/PulseInvalidation.ml index f921a39cf..d55518678 100644 --- a/infer/src/pulse/PulseInvalidation.ml +++ b/infer/src/pulse/PulseInvalidation.ml @@ -38,11 +38,11 @@ let pp_std_vector_function f = function type t = - | CFree of HilExp.AccessExpression.t * Location.t - | CppDelete of HilExp.AccessExpression.t * Location.t - | GoneOutOfScope of HilExp.AccessExpression.t * Location.t + | CFree of HilExp.AccessExpression.t + | CppDelete of HilExp.AccessExpression.t + | GoneOutOfScope of HilExp.AccessExpression.t | Nullptr - | StdVector of std_vector_function * HilExp.AccessExpression.t * Location.t + | StdVector of std_vector_function * HilExp.AccessExpression.t [@@deriving compare] let issue_type_of_cause = function @@ -59,14 +59,14 @@ let issue_type_of_cause = function let pp f = function - | CFree (access_expr, _) -> + | CFree access_expr -> F.fprintf f "by call to `free()` on `%a`" HilExp.AccessExpression.pp access_expr - | CppDelete (access_expr, _) -> + | CppDelete access_expr -> F.fprintf f "by `delete` on `%a`" HilExp.AccessExpression.pp access_expr - | GoneOutOfScope (access_expr, _) -> + | GoneOutOfScope access_expr -> F.fprintf f "`%a` gone out of scope" HilExp.AccessExpression.pp access_expr | Nullptr -> F.fprintf f "null pointer" - | StdVector (std_vector_f, access_expr, _) -> + | StdVector (std_vector_f, access_expr) -> F.fprintf f "potentially invalidated by call to `%a()` on `%a`" pp_std_vector_function std_vector_f HilExp.AccessExpression.pp access_expr diff --git a/infer/src/pulse/PulseInvalidation.mli b/infer/src/pulse/PulseInvalidation.mli index 951257ea2..86e09732b 100644 --- a/infer/src/pulse/PulseInvalidation.mli +++ b/infer/src/pulse/PulseInvalidation.mli @@ -20,11 +20,11 @@ type std_vector_function = val pp_std_vector_function : Format.formatter -> std_vector_function -> unit type t = - | CFree of HilExp.AccessExpression.t * Location.t - | CppDelete of HilExp.AccessExpression.t * Location.t - | GoneOutOfScope of HilExp.AccessExpression.t * Location.t + | CFree of HilExp.AccessExpression.t + | CppDelete of HilExp.AccessExpression.t + | GoneOutOfScope of HilExp.AccessExpression.t | Nullptr - | StdVector of std_vector_function * HilExp.AccessExpression.t * Location.t + | StdVector of std_vector_function * HilExp.AccessExpression.t [@@deriving compare] val issue_type_of_cause : t -> IssueType.t diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index 2319a6b2b..df428b095 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/infer/src/pulse/PulseModels.ml @@ -26,7 +26,7 @@ module C = struct match actuals with | [AccessExpression deleted_access] -> PulseOperations.invalidate - (PulseTrace.Immediate {imm= PulseInvalidation.CFree (deleted_access, location); location}) + (PulseTrace.Immediate {imm= PulseInvalidation.CFree deleted_access; location}) location deleted_access astate | _ -> Ok astate @@ -40,8 +40,7 @@ module Cplusplus = struct match actuals with | [AccessExpression deleted_access] -> PulseOperations.invalidate - (PulseTrace.Immediate - {imm= PulseInvalidation.CppDelete (deleted_access, location); location}) + (PulseTrace.Immediate {imm= PulseInvalidation.CppDelete deleted_access; location}) location deleted_access astate | _ -> Ok astate @@ -102,7 +101,7 @@ module StdVector = struct let array_address = to_internal_array vector in let array = deref_internal_array vector in let invalidation = - PulseTrace.Immediate {imm= PulseInvalidation.StdVector (vector_f, vector, location); location} + PulseTrace.Immediate {imm= PulseInvalidation.StdVector (vector_f, vector); location} in PulseOperations.invalidate_array_elements invalidation location array astate >>= PulseOperations.invalidate invalidation location array