From 8446ef488c7d44c8af3a0d1f2724f0c5170fb694 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Tue, 25 May 2021 09:09:11 -0700 Subject: [PATCH] [pulse][0/5] MustBeValid should be removed in the pre, not the post Summary: That was just broken before, but apparently nothing cared. It's needed for the next diffs. Reviewed By: skcho Differential Revision: D28674731 fbshipit-source-id: 2f080238b --- infer/src/pulse/PulseAbductiveDomain.ml | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index 8702154a7..00d1e26b6 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/infer/src/pulse/PulseAbductiveDomain.ml @@ -258,6 +258,12 @@ module AddressAttributes = struct if phys_equal new_post astate.post then astate else {astate with post= new_post} + (** [astate] with [astate.pre.attrs = f astate.pre.attrs] *) + let map_pre_attrs ~f astate = + let new_pre = PreDomain.update astate.pre ~attrs:(f (astate.pre :> base_domain).attrs) in + if phys_equal new_pre astate.pre then astate else {astate with pre= new_pre} + + let invalidate address invalidation location astate = let astate = map_post_attrs ~f:(BaseAddressAttributes.invalidate address invalidation location) astate @@ -294,7 +300,7 @@ module AddressAttributes = struct let remove_must_be_valid_attr address astate = - map_post_attrs astate ~f:(BaseAddressAttributes.remove_must_be_valid_attr address) + map_pre_attrs astate ~f:(BaseAddressAttributes.remove_must_be_valid_attr address) let get_closure_proc_name addr astate =