From c19e4c097e474d55f3f03884e08171556feb8cab Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Thu, 28 Sep 2023 12:01:27 +0200 Subject: [PATCH] Fix blobsize query compare --- src/domains/queries.ml | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/src/domains/queries.ml b/src/domains/queries.ml index eedbb3ac34..1a7ec2276d 100644 --- a/src/domains/queries.ml +++ b/src/domains/queries.ml @@ -337,7 +337,12 @@ struct | Any (EvalLength e1), Any (EvalLength e2) -> CilType.Exp.compare e1 e2 | Any (EvalMutexAttr e1), Any (EvalMutexAttr e2) -> CilType.Exp.compare e1 e2 | Any (EvalValue e1), Any (EvalValue e2) -> CilType.Exp.compare e1 e2 - | Any (BlobSize {exp = e1; _}), Any (BlobSize {exp = e2; _}) -> CilType.Exp.compare e1 e2 + | Any (BlobSize {exp = e1; base_address = b1}), Any (BlobSize {exp = e2; base_address = b2}) -> + let r = CilType.Exp.compare e1 e2 in + if r <> 0 then + r + else + Stdlib.compare b1 b2 | Any (CondVars e1), Any (CondVars e2) -> CilType.Exp.compare e1 e2 | Any (PartAccess p1), Any (PartAccess p2) -> compare_access p1 p2 | Any (IterPrevVars ip1), Any (IterPrevVars ip2) -> compare_iterprevvar ip1 ip2