package goblint

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
include Lattice.S with type t = [ `Top | `Int of ID.t | `Float of FD.t | `Address of AD.t | `Struct of Structs.t | `Union of Unions.t | `Array of CArrays.t | `Blob of Blobs.t | `Thread of Threads.t | `Mutex | `Bot ]
include Lattice.PO with type t = [ `Top | `Int of ID.t | `Float of FD.t | `Address of AD.t | `Struct of Structs.t | `Union of Unions.t | `Array of CArrays.t | `Blob of Blobs.t | `Thread of Threads.t | `Mutex | `Bot ]
include Printable.S with type t = [ `Top | `Int of ID.t | `Float of FD.t | `Address of AD.t | `Struct of Structs.t | `Union of Unions.t | `Array of CArrays.t | `Blob of Blobs.t | `Thread of Threads.t | `Mutex | `Bot ]
type t = [
  1. | `Top
  2. | `Int of ID.t
  3. | `Float of FD.t
  4. | `Address of AD.t
  5. | `Struct of Structs.t
  6. | `Union of Unions.t
  7. | `Array of CArrays.t
  8. | `Blob of Blobs.t
  9. | `Thread of Threads.t
  10. | `Mutex
  11. | `Bot
]
val equal : t -> t -> bool
val hash : t -> int
val compare : t -> t -> int
val show : t -> string
val pretty : unit -> t -> Goblint_lib.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) -> Goblint_lib.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
val eval_offset : Q.ask -> (AD.t -> t) -> t -> offs -> GoblintCil.exp option -> GoblintCil.lval option -> GoblintCil.typ -> t
val update_offset : Q.ask -> 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 -> Q.ask -> t -> GoblintCil.varinfo -> (GoblintCil.exp -> int option) -> t
val affecting_vars : t -> GoblintCil.varinfo list
val invalidate_value : Q.ask -> GoblintCil.typ -> t -> t
val is_safe_cast : GoblintCil.typ -> GoblintCil.typ -> bool
val cast : ?torg:GoblintCil.typ -> GoblintCil.typ -> t -> t
val smart_join : (GoblintCil.exp -> BI.t option) -> (GoblintCil.exp -> BI.t option) -> t -> t -> t
val smart_widen : (GoblintCil.exp -> BI.t option) -> (GoblintCil.exp -> BI.t option) -> t -> t -> t
val smart_leq : (GoblintCil.exp -> BI.t option) -> (GoblintCil.exp -> BI.t option) -> t -> t -> bool
val is_immediate_type : GoblintCil.typ -> bool
val bot_value : GoblintCil.typ -> t
val is_bot_value : t -> bool
val init_value : GoblintCil.typ -> t
val top_value : GoblintCil.typ -> t
val is_top_value : t -> GoblintCil.typ -> bool
val zero_init_value : GoblintCil.typ -> t
val project : PrecisionUtil.int_precision -> t -> t
OCaml

Innovation. Community. Security.