package goblint

  1. Overview
  2. Docs
package goblint
Legend:
Library
Module
Module type
Parameter
Class
Class type
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 int_t

Accessing values of the ADT

val bot_of : Cil.ikind -> t
val top_of : Cil.ikind -> t
val to_int : t -> int_t option

Return a single integer value if the value is a known constant, otherwise * don't return anything.

val is_int : t -> bool

Checks if the element is a definite integer value. If this function * returns true, the above to_int should return a real value.

val equal_to : int_t -> t -> [ `Eq | `Neq | `Top ]
val to_bool : t -> bool option

Give a boolean interpretation of an abstract value if possible, otherwise * don't return anything.

val is_bool : t -> bool

Checks if the element is a definite boolean value. If this function * returns true, the above to_bool should return a real value.

val to_excl_list : t -> int_t list option

Gives a list representation of the excluded values if possible.

val of_excl_list : Cil.ikind -> int_t list -> t

Creates an exclusion set from a given list of integers.

val is_excl_list : t -> bool

Checks if the element is an exclusion set.

val to_incl_list : t -> int_t list option

Gives a list representation of the included values if possible.

val maximal : t -> int_t option
val minimal : t -> int_t option

Cast

val cast_to : ?torg:Cil.typ -> Cil.ikind -> t -> t

Cast from original type torg to integer type Cil.ikind. Currently, torg is only present for actual casts. The function is also called to handle overflows/wrap around after operations. In these cases (where the type stays the same) torg is None.

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct