Skip to content

Commit

Permalink
Improve history thread ID may_create for incompatible prefixes
Browse files Browse the repository at this point in the history
  • Loading branch information
sim642 committed Aug 14, 2024
1 parent 52055b1 commit baa497a
Showing 1 changed file with 3 additions and 1 deletion.
4 changes: 3 additions & 1 deletion src/cdomain/value/cdomains/threadIdDomain.ml
Original file line number Diff line number Diff line change
Expand Up @@ -154,7 +154,9 @@ struct
if is_unique t' then
is_must_parent t t' (* unique must be created by something unique (that's a prefix) *)
else
S.subset (S.union (S.of_list p) s) (S.union (S.of_list p') s')
let cdef_ancestor = P.common_suffix p p' in
(P.equal cdef_ancestor p || P.equal cdef_ancestor p') && (* prefixes must not be incompatible (one is prefix of another or vice versa), because compose cannot fix incompatibility there *)
S.subset (S.union (S.of_list p) s) (S.union (S.of_list p') s') (* elements must be contained, because compose can only add them *)

let compose ((p, s) as current) ni =
if BatList.mem_cmp Base.compare ni p then (
Expand Down

0 comments on commit baa497a

Please sign in to comment.