From a107b2dd2dff4b857ccc70e7a4275e96f556fc91 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Fri, 15 Nov 2019 07:46:32 -0800 Subject: [PATCH] [pulse] do not invalidate object *values* on destruction Summary: This was causing loads of false positives later in the stack. Invalidating the address of the object seems to be enough here as it doesn't break any tests. Reviewed By: ezgicicek Differential Revision: D18246090 fbshipit-source-id: 2ef9a6a5c --- infer/src/pulse/Pulse.ml | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml index b92821b70..5a922898e 100644 --- a/infer/src/pulse/Pulse.ml +++ b/infer/src/pulse/Pulse.ml @@ -92,11 +92,10 @@ module PulseTransferFunctions = struct (** [out_of_scope_access_expr] has just gone out of scope and in now invalid *) let exec_object_out_of_scope call_loc (pvar, typ) astate = let gone_out_of_scope = Invalidation.GoneOutOfScope (pvar, typ) in - (* invalidate both [&x] and [x]: reading either is now forbidden *) + (* invalidate [&x] *) PulseOperations.eval call_loc (Exp.Lvar pvar) astate >>= fun (astate, out_of_scope_base) -> - PulseOperations.invalidate_deref call_loc gone_out_of_scope out_of_scope_base astate - >>= PulseOperations.invalidate call_loc gone_out_of_scope out_of_scope_base + PulseOperations.invalidate call_loc gone_out_of_scope out_of_scope_base astate let dispatch_call tenv summary ret call_exp actuals call_loc flags astate =