From a18e22ef7f9e9255be34de6c19ec8eaadfac42f4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ezgi=20=C3=87i=C3=A7ek?= Date: Fri, 30 Aug 2019 08:23:39 -0700 Subject: [PATCH] [pulse] Remove empty edges and their WrittenTo from post Summary: Like we removed empty edges from the `pre_heap` in D16419183, let's do the same to `post_heap`. Reviewed By: skcho Differential Revision: D17111336 fbshipit-source-id: c35fcbabb --- infer/src/pulse/PulseAbductiveDomain.ml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index 46f41781f..e1cd3b5f0 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/infer/src/pulse/PulseAbductiveDomain.ml @@ -296,14 +296,14 @@ module PrePost = struct (fun var _ -> Var.appears_in_source_code var && not (is_local var astate)) (astate.post :> PulseDomain.t).stack in - (* deregister empty edges in pre *) - let pre_heap = - BaseMemory.filter_heap - (fun _addr edges -> not (BaseMemory.Edges.is_empty edges)) - (astate.pre :> base_domain).heap + (* deregister empty edges *) + let deregister_empty heap = + BaseMemory.filter_heap (fun _addr edges -> not (BaseMemory.Edges.is_empty edges)) heap in + let pre_heap = deregister_empty (astate.pre :> base_domain).heap in + let post_heap = deregister_empty (astate.post :> base_domain).heap in { pre= InvertedDomain.update astate.pre ~heap:pre_heap - ; post= Domain.update ~stack:post_stack astate.post } + ; post= Domain.update ~stack:post_stack ~heap:post_heap astate.post } let add_out_of_scope_attribute addr pvar location history heap typ =