Module ValueDomain.Compound

include Lattice.S with type t = [ `Top | `Int of ID.t | `Address of AD.t | `Struct of Structs.t | `Union of Unions.t | `Array of CArrays.t | `Blob of Blobs.t | `List of Lists.t | `Thread of Threads.t | `Bot ]
include Lattice.PO with type t = [ `Top | `Int of ID.t | `Address of AD.t | `Struct of Structs.t | `Union of Unions.t | `Array of CArrays.t | `Blob of Blobs.t | `List of Lists.t | `Thread of Threads.t | `Bot ]
include Printable.S with type t = [ `Top | `Int of ID.t | `Address of AD.t | `Struct of Structs.t | `Union of Unions.t | `Array of CArrays.t | `Blob of Blobs.t | `List of Lists.t | `Thread of Threads.t | `Bot ]
type t = [
  1. | `Top
  2. | `Int of ID.t
  3. | `Address of AD.t
  4. | `Struct of Structs.t
  5. | `Union of Unions.t
  6. | `Array of CArrays.t
  7. | `Blob of Blobs.t
  8. | `List of Lists.t
  9. | `Thread of Threads.t
  10. | `Bot
]
val equal : t -> t -> bool
val hash : t -> int
val compare : t -> t -> int
val show : t -> string
val pretty : unit -> t -> Pretty.doc
val printXml : 'a BatInnerIO.output -> t -> unit
val name : unit -> string
val to_yojson : t -> Printable.json
val invariant : Invariant.context -> t -> Invariant.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) -> 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 = (Cil.fieldinfo, IndexDomain.t) Lval.offs
val eval_offset : Q.ask -> (AD.t -> t) -> t -> offs -> Cil.exp option -> Cil.lval option -> Cil.typ -> t
val update_offset : Q.ask -> t -> offs -> t -> Cil.exp option -> Cil.lval -> Cil.typ -> t
val update_array_lengths : (Cil.exp -> t) -> t -> Cil.typ -> t
val affect_move : ?replace_with_const:bool -> Q.ask -> t -> Cil.varinfo -> (Cil.exp -> int option) -> t
val affecting_vars : t -> Cil.varinfo list
val invalidate_value : Q.ask -> Cil.typ -> t -> t
val is_safe_cast : Cil.typ -> Cil.typ -> bool
val cast : ?torg:Cil.typ -> Cil.typ -> t -> t
val smart_join : (Cil.exp -> int64 option) -> (Cil.exp -> int64 option) -> t -> t -> t
val smart_widen : (Cil.exp -> int64 option) -> (Cil.exp -> int64 option) -> t -> t -> t
val smart_leq : (Cil.exp -> int64 option) -> (Cil.exp -> int64 option) -> t -> t -> bool
val is_immediate_type : Cil.typ -> bool
val bot_value : Cil.typ -> t
val init_value : Cil.typ -> t
val top_value : Cil.typ -> t
val zero_init_value : Cil.typ -> t