Merge pull request #1405 from goblint/issue_1386

Improve output for `NullByte`

Author: michael-schwarz

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 ())

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