From b85ed973887968ad5bacd2fab9f296c45e7205aa Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sun, 26 Nov 2023 18:08:12 +0100 Subject: [PATCH] Progress --- src/cdomains/arrayDomain.ml | 10 +++++----- src/cdomains/nullByteSet.ml | 2 ++ 2 files changed, 7 insertions(+), 5 deletions(-) diff --git a/src/cdomains/arrayDomain.ml b/src/cdomains/arrayDomain.ml index ae6c35a6e0..3edfb4d207 100644 --- a/src/cdomains/arrayDomain.ml +++ b/src/cdomains/arrayDomain.ml @@ -1234,7 +1234,7 @@ struct | Some i -> build_set (i + 1) (MaySet.add (Z.of_int i) set) | None -> MaySet.add last_null set in let set = build_set 0 (MaySet.empty ()) in - ((set, set), Idx.of_int ILong (Z.succ last_null)) + (Nulls.precise_set set, Idx.of_int ILong (Z.succ last_null)) (** Returns an abstract value with at most one null byte marking the end of the string *) let to_string ((nulls, size) as x:t):t = @@ -1579,10 +1579,10 @@ struct let n = Z.of_int n in (* take at most n bytes from src; if no null byte among them, add null byte at index n *) let nulls2' = - let (must_nulls_set2, may_nulls_set2), size2 = to_string (nulls2, size2) in - if not (MaySet.exists (Z.gt n) may_nulls_set2) then - (Nulls.precise_singleton n) - else if not (MustSet.exists (Z.gt n) must_nulls_set2) then + let ((must_nulls_set2, may_nulls_set2) as nulls2), size2 = to_string (nulls2, size2) in + if not (Nulls.exists Possibly (Z.gt n) nulls2) then + Nulls.precise_singleton n + else if not (Nulls.exists Definitely (Z.gt n) nulls2) then let max_size2 = BatOption.default (Z.succ n) (idx_maximal size2) in (MustSet.empty (), MaySet.add n (MaySet.filter (Z.geq n) may_nulls_set2 max_size2)) else diff --git a/src/cdomains/nullByteSet.ml b/src/cdomains/nullByteSet.ml index 283b15306c..320126b517 100644 --- a/src/cdomains/nullByteSet.ml +++ b/src/cdomains/nullByteSet.ml @@ -146,6 +146,8 @@ module MustMaySet = struct let precise_singleton i = (MustSet.singleton i, MaySet.singleton i) + let precise_set s = (s,s) + let make_all_must () = (MustSet.bot (), MaySet.top ()) let make_none_may () = (MustSet.top (), MaySet.bot ())