From 20ee375f30ee5072fdfd1f7340fc4dd85358ebe6 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Tue, 28 Nov 2023 21:05:29 +0100 Subject: [PATCH] One less May/MustSet --- src/cdomains/arrayDomain.ml | 13 +++++-------- src/cdomains/nullByteSet.ml | 2 ++ 2 files changed, 7 insertions(+), 8 deletions(-) diff --git a/src/cdomains/arrayDomain.ml b/src/cdomains/arrayDomain.ml index 7cadd66c19..7818f5ac85 100644 --- a/src/cdomains/arrayDomain.ml +++ b/src/cdomains/arrayDomain.ml @@ -1395,14 +1395,11 @@ struct (if min_size1 <. min_len2 then warn_past_end "The length of string src may be greater than the allocated size for dest"); (* do not keep any index of dest as no maximal strlen of src *) - let must_nulls_set_result = - let min_size2 = BatOption.default Z.zero (Idx.minimal truncatedsize) in - MustSet.filter ~min_size:min_size2 (Z.gt min_size1) must_nulls_set2' in - let may_nulls_set_result = - (* get all may nulls from src string as no maximal size of dest *) - may_nulls_set2' - |> MaySet.union (MaySet.filter ~max_size:(Z.succ min_len2) (Z.leq min_len2) may_nulls_set1) in - ((must_nulls_set_result, may_nulls_set_result), dstsize) + let min_size2 = BatOption.default Z.zero (Idx.minimal truncatedsize) in + let truncatednulls = Nulls.remove_interval Possibly (Z.zero, min_size1) min_size2 truncatednulls in + let filtered_dst = Nulls.filter ~max_size:(Z.succ min_len2) (Z.leq min_len2) dstnulls in + (* get all may nulls from src string as no maximal size of dest *) + (Nulls.union_mays truncatednulls filtered_dst, dstsize) (* any other case shouldn't happen as minimal index is always >= 0 *) | _ -> (Nulls.top (), dstsize) in diff --git a/src/cdomains/nullByteSet.ml b/src/cdomains/nullByteSet.ml index 54284f6ab5..53196bb43c 100644 --- a/src/cdomains/nullByteSet.ml +++ b/src/cdomains/nullByteSet.ml @@ -170,6 +170,8 @@ module MustMaySet = struct | Definitely ->failwith "todo" | Possibly -> MaySet.elements ?max_size mays + let union_mays (must,mays) (_,mays2) = (must, MaySet.join mays mays2) + let precise_singleton i = (MustSet.singleton i, MaySet.singleton i)