diff --git a/src/cdomain/value/cdomains/arrayDomain.ml b/src/cdomain/value/cdomains/arrayDomain.ml index 8958ee2303..e1cfb96425 100644 --- a/src/cdomain/value/cdomains/arrayDomain.ml +++ b/src/cdomain/value/cdomains/arrayDomain.ml @@ -1012,9 +1012,9 @@ struct let (+.) = Z.add (* (Must Null Set, May Null Set, Array Size) *) - include Lattice.Prod (Nulls) (Idx) + include Lattice.Prod (Nulls) (struct include Idx let name () = "length" end) - let name () = "arrays containing null bytes" + let name () = "ArrayNullBytes" type idx = Idx.t type value = Val.t @@ -1815,6 +1815,17 @@ struct else f_get + let delegate_if_no_nullbytes (a, n) ffull fa = + if get_bool "ana.base.arrays.nullbytes" then + ffull (a, n) + else + fa a + + let show x = delegate_if_no_nullbytes x show A.show + let printXml f x = delegate_if_no_nullbytes x (printXml f) (A.printXml f) + let to_yojson x = delegate_if_no_nullbytes x to_yojson A.to_yojson + let pretty () x = delegate_if_no_nullbytes x (pretty ()) (A.pretty ()) + let construct a n = if get_bool "ana.base.arrays.nullbytes" then (a, n ()) diff --git a/src/cdomain/value/cdomains/nullByteSet.ml b/src/cdomain/value/cdomains/nullByteSet.ml index ae382b6118..87dcac7f2d 100644 --- a/src/cdomain/value/cdomains/nullByteSet.ml +++ b/src/cdomain/value/cdomains/nullByteSet.ml @@ -4,6 +4,8 @@ module MustSet = struct module M = SetDomain.Reverse (SetDomain.ToppedSet (IntOps.BigIntOps) (struct let topname = "All Null" end)) include M + let name () = "MustNullBytes" + let compute_set len = List.init (Z.to_int len) Z.of_int |> of_list @@ -48,6 +50,8 @@ module MaySet = struct module M = SetDomain.ToppedSet (IntOps.BigIntOps) (struct let topname = "All Null" end) include M + let name () = "MayNullBytes" + let elements ?max_size may_nulls_set = if M.is_top may_nulls_set then match max_size with