From 5f1b296dec23ce3418737c7f956f71e36d1fdc7f Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 15 Aug 2024 13:17:13 +0300 Subject: [PATCH] Clean up history thread ID is_must_parent --- src/cdomain/value/cdomains/threadIdDomain.ml | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/src/cdomain/value/cdomains/threadIdDomain.ml b/src/cdomain/value/cdomains/threadIdDomain.ml index 466b8ae72b..7e208cba0e 100644 --- a/src/cdomain/value/cdomains/threadIdDomain.ml +++ b/src/cdomain/value/cdomains/threadIdDomain.ml @@ -140,16 +140,16 @@ struct let is_unique (_, s) = S.is_empty s - let is_must_parent (p,s) (p',s') = - if not (S.is_empty s) then + let is_must_parent ((p, s) as t) ((p', s') as t') = + if not (is_unique t) then false - else if P.equal p' p && S.is_empty s' then (* s is already empty *) - (* We do not consider a thread its own parent *) - false - else + 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 *) match GobList.remove_common_prefix Base.equal (List.rev p) (List.rev p') with (* prefixes are stored reversed *) - | [], _ -> true + | [], _ -> true (* p is prefix of p' *) | _ :: _, _ -> false + ) let may_create ((p, s) as t) ((p', s') as t') = if is_unique t' then