package goblint

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

Module IntDomain.FlatPureIntegers

The integers with flattened orderings. Calling top and bot or joining or meeting inequal elements will raise exceptions.

include IntDomain_intf.B with type t = IntOps.Int64Ops.t with type int_t = IntOps.Int64Ops.t
include Lattice.PO with type t = IntOps.Int64Ops.t
include Printable.S with type t = IntOps.Int64Ops.t
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 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) -> Lattice.Pretty.doc

If leq x y = false, then pretty_diff () (x, y) should explain why.

include Lattice.Bot with type t := t
val bot : unit -> t
val is_bot : t -> bool
type int_t = IntOps.Int64Ops.t

Accessing values of the ADT

val bot_of : GoblintCil.Cil.ikind -> t
val top_of : ?bitfield:int -> 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 * (int * int)) 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 : ?suppress_ovwarn:bool -> kind:GoblintCil.castkind -> GoblintCil.Cil.ikind -> t -> t

Cast to Cil.ikind. The function is also called to handle overflow/wraparound after operations.

include Lattice.Top with type t := t
val top : unit -> t
val is_top : t -> bool
include IntDomain_intf.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 -> bool option

Less than: x < y

val gt : t -> t -> bool option

Greater than: x > y

val le : t -> t -> bool option

Less than or equal: x <= y

val ge : t -> t -> bool option

Greater than or equal: x >= y

val eq : t -> t -> bool option

Equal to: x == y

val ne : t -> t -> bool option

Not equal to: x != y

Bitwise logical operators

val lognot : t -> t

Bitwise logical not (one's complement): ~x

val logand : t -> t -> t

Bitwise logical and: x & y

val logor : t -> t -> t

Bitwise logical or: x | y

val logxor : t -> t -> t

Bitwise logical 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

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