package goblint

  1. Overview
  2. Docs
package goblint
Legend:
Library
Module
Module type
Parameter
Class
Class type

This is the typical flattened integer domain used in Kildall's constant * propagation.

include B with type t = [ `Top | `Lifted of IntOps.Int64Ops.t | `Bot ] with type int_t = IntOps.Int64Ops.t
include Lattice.S with type t = [ `Top | `Lifted of IntOps.Int64Ops.t | `Bot ]
include Lattice.PO with type t = [ `Top | `Lifted of IntOps.Int64Ops.t | `Bot ]
include Printable.S with type t = [ `Top | `Lifted of IntOps.Int64Ops.t | `Bot ]
type t = [
  1. | `Top
  2. | `Lifted of IntOps.Int64Ops.t
  3. | `Bot
]
val equal : t -> t -> bool
val hash : t -> int
val compare : t -> t -> int
val show : t -> string
val pretty : unit -> t -> GoblintCil.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 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) -> GoblintCil.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.Int64Ops.t

Accessing values of the ADT

val bot_of : GoblintCil.Cil.ikind -> t
val top_of : GoblintCil.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 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 to_excl_list : t -> (int_t list * (int64 * int64)) option

Gives a list representation of the excluded values from included range of bits if possible.

val of_excl_list : GoblintCil.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:GoblintCil.Cil.typ -> GoblintCil.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.

include Arith with type t := t
val neg : t -> t

Negating an integer value: -x

val add : t -> t -> t

Addition: x + y

val sub : t -> t -> t

Subtraction: x - y

val mul : t -> t -> t

Multiplication: x * y

val div : t -> t -> t

Division: x / y

val rem : t -> t -> t

Integer remainder: x % y

Comparison operators

val lt : t -> t -> t

Less than: x < y

val gt : t -> t -> t

Greater than: x > y

val le : t -> t -> t

Less than or equal: x <= y

val ge : t -> t -> t

Greater than or equal: x >= y

val eq : t -> t -> t

Equal to: x == y

val ne : t -> t -> t

Not equal to: x != y

Bit operators

val bitnot : t -> t

Bitwise not (one's complement): ~x

val bitand : t -> t -> t

Bitwise and: x & y

val bitor : t -> t -> t

Bitwise or: x | y

val bitxor : t -> t -> t

Bitwise exclusive or: x ^ y

val shift_left : t -> t -> t

Shifting bits left: x << y

val shift_right : t -> t -> t

Shifting bits right: x >> y

Logical operators

val lognot : t -> t

Logical not: !x

val logand : t -> t -> t

Logical and: x && y

val logor : t -> t -> t

Logical or: x || y

val starting : ?suppress_ovwarn:bool -> GoblintCil.Cil.ikind -> int_t -> t
val ending : ?suppress_ovwarn:bool -> GoblintCil.Cil.ikind -> int_t -> t
val of_int : int_t -> t

Transform an integer literal to your internal domain representation.

val of_bool : bool -> t

Transform a known boolean value to the default internal representation. It * should follow C: of_bool true = of_int 1 and of_bool false = of_int 0.

val of_interval : ?suppress_ovwarn:bool -> GoblintCil.Cil.ikind -> (int_t * int_t) -> t
val of_congruence : GoblintCil.Cil.ikind -> (int_t * int_t) -> t
val arbitrary : unit -> t QCheck.arbitrary
val invariant : GoblintCil.Cil.exp -> t -> Invariant.t
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