Module type ValueDomain.S

include Lattice.S
include Lattice.PO
include Printable.S
type t
val equal : t -> t -> bool
val hash : t -> int
val compare : t -> t -> int
val show : t -> string
val pretty : unit -> t -> Printable.Pretty.doc
val printXml : 'a BatInnerIO.output -> t -> unit
val name : unit -> string
val to_yojson : t -> Yojson.Safe.t
val tag : t -> int

Unique ID, given by HConsed, for context identification in witness

val arbitrary : unit -> t QCheck.arbitrary
val relift : t -> t
val leq : t -> t -> bool
val join : t -> t -> t
val meet : t -> t -> t
val widen : t -> t -> t

widen x y assumes leq x y. Solvers guarantee this by calling widen old (join old new).

val narrow : t -> t -> t
val pretty_diff : unit -> (t * t) -> Lattice.Pretty.doc

If leq x y = false, then pretty_diff () (x, y) should explain why.

val bot : unit -> t
val is_bot : t -> bool
val top : unit -> t
val is_top : t -> bool
type offs
val eval_offset : VDQ.t -> (AD.t -> t) -> t -> offs -> GoblintCil.exp option -> GoblintCil.lval option -> GoblintCil.typ -> t
val update_offset : ?blob_destructive:bool -> VDQ.t -> t -> offs -> t -> GoblintCil.exp option -> GoblintCil.lval -> GoblintCil.typ -> t
val update_array_lengths : (GoblintCil.exp -> t) -> t -> GoblintCil.Cil.typ -> t
val affect_move : ?replace_with_const:bool -> VDQ.t -> t -> GoblintCil.varinfo -> (GoblintCil.exp -> int option) -> t
val affecting_vars : t -> GoblintCil.varinfo list
val invalidate_value : VDQ.t -> GoblintCil.typ -> t -> t
val invalidate_abstract_value : t -> t
val is_statically_safe_cast : GoblintCil.typ -> GoblintCil.typ -> bool
val is_dynamically_safe_cast : GoblintCil.typ -> GoblintCil.typ -> t -> bool
val cast : ?torg:GoblintCil.typ -> GoblintCil.typ -> t -> t
val smart_join : (GoblintCil.exp -> Z.t option) -> (GoblintCil.exp -> Z.t option) -> t -> t -> t
val smart_widen : (GoblintCil.exp -> Z.t option) -> (GoblintCil.exp -> Z.t option) -> t -> t -> t
val smart_leq : (GoblintCil.exp -> Z.t option) -> (GoblintCil.exp -> Z.t option) -> t -> t -> bool
val is_immediate_type : GoblintCil.typ -> bool
val is_mutex_type : GoblintCil.typ -> bool
val bot_value : ?varAttr:GoblintCil.attributes -> GoblintCil.typ -> t
val is_bot_value : t -> bool
val init_value : ?varAttr:GoblintCil.attributes -> GoblintCil.typ -> t
val top_value : ?varAttr:GoblintCil.attributes -> GoblintCil.typ -> t
val is_top_value : t -> GoblintCil.typ -> bool
val zero_init_value : ?varAttr:GoblintCil.attributes -> GoblintCil.typ -> t
include ArrayDomain.Null with type t := t
type retnull =
  1. | Null
  2. | NotNull
  3. | Maybe
val null : unit -> t
val is_null : t -> retnull
val get_ikind : t -> GoblintCil.Cil.ikind option
val zero_of_ikind : GoblintCil.Cil.ikind -> t
val not_zero_of_ikind : GoblintCil.Cil.ikind -> t
val project : VDQ.t -> PrecisionUtil.int_precision option -> (GoblintCil.attributes * GoblintCil.attributes) option -> t -> t
val mark_jmpbufs_as_copied : t -> t