diff --git a/src/cdomain/value/cdomains/threadIdDomain.ml b/src/cdomain/value/cdomains/threadIdDomain.ml index 7e208cba0e..b7216b4f39 100644 --- a/src/cdomain/value/cdomains/threadIdDomain.ml +++ b/src/cdomain/value/cdomains/threadIdDomain.ml @@ -145,7 +145,7 @@ struct false else if is_unique t' && P.equal p p' then (* t is already unique, so no need to compare sets *) false (* thread is not its own parent *) - else ( (* both are unique, but different *) + else ( (* t is already unique, so no need to check sets *) match GobList.remove_common_prefix Base.equal (List.rev p) (List.rev p') with (* prefixes are stored reversed *) | [], _ -> true (* p is prefix of p' *) | _ :: _, _ -> false @@ -169,6 +169,9 @@ struct false (* composing cannot fix incompatibility there *) ) + (* let may_create ((p, s) as t) ((p', s') as t') = + S.subset (S.union (S.of_list p) s) (S.union (S.of_list p') s') *) + let compose ((p, s) as current) ni = if BatList.mem_cmp Base.compare ni p then ( let shared, unique = BatList.span (not % Base.equal ni) p in