package goblint
Install
Dune Dependency
Authors
Maintainers
Sources
sha256=dba2b664c7c125687e708e871d83fbfb6ba6d9ee98d235b4850d9a238caa84de
sha512=529987cde39691ad9e955000a3603e89c1c8cf14ed5e8b4cd3a7fc26e47d016aff571b472e2329725133c46f8d0cb45a05b88994eeffaa221a4d31b4c543adcd
doc/goblint.lib/Goblint_lib/Lval/Offset/argument-1-Idx/index.html
Parameter Offset.Idx
include IntDomain.B with type int_t = IntOps.BigIntOps.t
include Lattice.S
include Lattice.PO
include Printable.S
val hash : t -> int
val show : t -> string
val pretty : unit -> t -> Goblint_lib.Printable.Pretty.doc
val printXml : 'a BatInnerIO.output -> t -> unit
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
widen x y
assumes leq x y
. Solvers guarantee this by calling widen old (join old new)
.
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
type int_t = IntOps.BigIntOps.t
Accessing values of the ADT
val bot_of : GoblintCil.Cil.ikind -> t
val top_of : GoblintCil.Cil.ikind -> t
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 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.
Gives a list representation of the excluded values from included range of bits if possible.
Creates an exclusion set from a given list of integers.
val is_excl_list : t -> bool
Checks if the element is an exclusion set.
Gives a list representation of the included values if possible.
Cast
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.
Transform an integer literal to your internal domain representation with the specified ikind.
val of_bool : GoblintCil.Cil.ikind -> bool -> t
Transform a known boolean value to the default internal representation of the specified ikind. It * should follow C: of_bool true = of_int 1
and of_bool false = of_int 0
.
val is_top_of : GoblintCil.Cil.ikind -> t -> bool
val project : PrecisionUtil.int_precision -> t -> t
val invariant : GoblintCil.Cil.exp -> t -> Invariant.t