Add StringDomain interface

Author: sim642

src/cdomains/addressDomain_intf.ml

@@ -7,7 +7,7 @@ sig
       | Addr of Mval.t (** Pointer to mvalue. *)
       | NullPtr (** NULL pointer. *)
       | UnknownPtr (** Unknown pointer. Could point to globals, heap and escaped variables. *)
-      | StrPtr of string option (** String literal pointer. [StrPtr None] abstracts any string pointer *)
+      | StrPtr of StringDomain.t (** String literal pointer. [StrPtr None] abstracts any string pointer *)
     include Printable.S with type t := t (** @closed *)
 
     val of_string: string -> t
@@ -16,8 +16,6 @@ sig
     val to_string: t -> string option
     (** Convert {!StrPtr} to string if possible. *)
 
-    (** C strings are different from OCaml strings as they are not processed after the first [NUL] byte, even though the OCaml string (and a C string literal) may be longer. *)
-
     val to_c_string: t -> string option
     (** Convert {!StrPtr} to C string if possible. *)
 

src/cdomains/stringDomain.ml

@@ -1,3 +1,7 @@
+include Printable.StdLeaf
+
+let name () = "string"
+
 type t = string option [@@deriving eq, ord, hash]
 
 let hash x =

src/cdomains/stringDomain.mli

@@ -0,0 +1,37 @@
+(** String literals domain. *)
+
+include Printable.S
+
+val of_string: string -> t
+(** Convert from string. *)
+
+val to_string: t -> string option
+(** Convert to string if possible. *)
+
+(** C strings are different from OCaml strings as they are not processed after the first [NUL] byte, even though the OCaml string (and a C string literal) may be longer. *)
+
+val to_c_string: t -> string option
+(** Convert to C string if possible. *)
+
+val to_n_c_string: int -> t -> string option
+(** Convert to C string of given maximum length if possible. *)
+
+val to_string_length: t -> int option
+(** Find length of C string if possible. *)
+
+val to_exp: t -> GoblintCil.exp
+(** Convert to CIL expression. *)
+
+val semantic_equal: t -> t -> bool option
+(** Check semantic equality of two strings.
+
+    @return [Some true] if definitely equal, [Some false] if definitely not equal, [None] if unknown. *)
+
+(** Some {!Lattice.S} operations. *)
+
+val leq: t -> t -> bool
+val join: t -> t -> t
+val meet: t -> t -> t
+
+val repr : t -> t
+(** Representative for address lattice. *)

src/goblint_lib.ml

@@ -211,6 +211,7 @@ module FloatDomain = FloatDomain
 
 module Mval = Mval
 module Offset = Offset
+module StringDomain = StringDomain
 module AddressDomain = AddressDomain
 
 (** {5 Complex} *)