Skip to content

Commit

Permalink
Fix ReachableFrom not adding back unknown pointer
Browse files Browse the repository at this point in the history
Regression from f7b38a0.
  • Loading branch information
sim642 committed Sep 19, 2023
1 parent c5136d1 commit 83978e9
Showing 1 changed file with 5 additions and 1 deletion.
6 changes: 5 additions & 1 deletion src/analyses/base.ml
Original file line number Diff line number Diff line change
Expand Up @@ -1287,7 +1287,11 @@ struct
| Address a ->
let a' = AD.remove Addr.UnknownPtr a in (* run reachable_vars without unknown just to be safe: TODO why? *)
let addrs = reachable_vars (Analyses.ask_of_ctx ctx) [a'] ctx.global ctx.local in
List.fold_left (AD.join) (AD.empty ()) addrs
let addrs' = List.fold_left (AD.join) (AD.empty ()) addrs in
if AD.may_be_unknown a then
AD.add UnknownPtr addrs' (* add unknown back *)
else
addrs'
| _ -> AD.empty ()
end
| Q.ReachableUkTypes e -> begin
Expand Down

1 comment on commit 83978e9

@michael-schwarz
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This change somehow causes Goblint to not be able to confirm almost any relational information in https://github.com/goblint/bench/blob/master/pthread/pfscan_comb_traces_rel.yml. 😞

Please sign in to comment.