Parameter Blob.Value

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