package goblint

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

Parameters

Signature

include S with type int_t = Ints_t.t with type t = (Ints_t.t * Ints_t.t) list
include B with type int_t = Ints_t.t with type t = (Ints_t.t * Ints_t.t) list
include Lattice.S with type t = (Ints_t.t * Ints_t.t) list
include Lattice.PO with type t = (Ints_t.t * Ints_t.t) list
include Printable.S with type t = (Ints_t.t * Ints_t.t) list
type t = (Ints_t.t * Ints_t.t) list
val equal : t -> t -> bool
val hash : t -> int
val compare : t -> t -> int
val show : t -> string
val pretty : unit -> t -> 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 relift : t -> t
val leq : t -> t -> bool
val pretty_diff : unit -> (t * t) -> 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 = Ints_t.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

include ArithIkind with type t := t
val rem : GoblintCil.Cil.ikind -> t -> t -> t

Integer remainder: x % y

Comparison operators

val lt : GoblintCil.Cil.ikind -> t -> t -> t

Less than: x < y

val gt : GoblintCil.Cil.ikind -> t -> t -> t

Greater than: x > y

val le : GoblintCil.Cil.ikind -> t -> t -> t

Less than or equal: x <= y

val ge : GoblintCil.Cil.ikind -> t -> t -> t

Greater than or equal: x >= y

val eq : GoblintCil.Cil.ikind -> t -> t -> t

Equal to: x == y

val ne : GoblintCil.Cil.ikind -> t -> t -> t

Not equal to: x != y

Bit operators

val lognot : GoblintCil.Cil.ikind -> t -> t

Bitwise not (one's complement): ~x

val logand : GoblintCil.Cil.ikind -> t -> t -> t

Bitwise and: x & y

val logor : GoblintCil.Cil.ikind -> t -> t -> t

Bitwise or: x | y

val logxor : GoblintCil.Cil.ikind -> t -> t -> t

Bitwise exclusive or: x ^ y

Logical operators

val c_lognot : GoblintCil.Cil.ikind -> t -> t

Logical not: !x

val c_logand : GoblintCil.Cil.ikind -> t -> t -> t

Logical and: x && y

val c_logor : GoblintCil.Cil.ikind -> t -> t -> t

Logical or: x || y

val join : GoblintCil.Cil.ikind -> t -> t -> t
val meet : GoblintCil.Cil.ikind -> t -> t -> t
val narrow : GoblintCil.Cil.ikind -> t -> t -> t
val widen : GoblintCil.Cil.ikind -> t -> t -> t
val of_bool : GoblintCil.Cil.ikind -> 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_congruence : GoblintCil.Cil.ikind -> (int_t * int_t) -> t
val is_top_of : GoblintCil.Cil.ikind -> t -> bool
val invariant_ikind : GoblintCil.Cil.exp -> GoblintCil.Cil.ikind -> t -> Invariant.t
val refine_with_congruence : GoblintCil.Cil.ikind -> t -> (int_t * int_t) option -> t
val refine_with_interval : GoblintCil.Cil.ikind -> t -> (int_t * int_t) option -> t
val refine_with_excl_list : GoblintCil.Cil.ikind -> t -> (int_t list * (int64 * int64)) option -> t
val refine_with_incl_list : GoblintCil.Cil.ikind -> t -> int_t list option -> t
val arbitrary : GoblintCil.Cil.ikind -> t QCheck.arbitrary
val add : ?no_ov:bool -> GoblintCil.Cil.ikind -> t -> t -> t * overflow_info
val sub : ?no_ov:bool -> GoblintCil.Cil.ikind -> t -> t -> t * overflow_info
val mul : ?no_ov:bool -> GoblintCil.Cil.ikind -> t -> t -> t * overflow_info
val div : ?no_ov:bool -> GoblintCil.Cil.ikind -> t -> t -> t * overflow_info
val neg : ?no_ov:bool -> GoblintCil.Cil.ikind -> t -> t * overflow_info
val cast_to : ?suppress_ovwarn:bool -> ?torg:GoblintCil.Cil.typ -> ?no_ov:bool -> GoblintCil.Cil.ikind -> t -> t * overflow_info
val of_interval : ?suppress_ovwarn:bool -> GoblintCil.Cil.ikind -> (int_t * int_t) -> t * overflow_info
val starting : ?suppress_ovwarn:bool -> GoblintCil.Cil.ikind -> int_t -> t * overflow_info
val ending : ?suppress_ovwarn:bool -> GoblintCil.Cil.ikind -> int_t -> t * overflow_info
val shift_left : GoblintCil.Cil.ikind -> t -> t -> t * overflow_info
val shift_right : GoblintCil.Cil.ikind -> t -> t -> t * overflow_info
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