IntDomain0 (p.goblint.2.6.0.doc.goblint_cdomain

include module type of struct include IntDomain_intf end

module type Arith = IntDomain_intf.Arith

module type ArithIkind = IntDomain_intf.ArithIkind

module type B = IntDomain_intf.B

The signature of integral value domains. They need to support all integer * operations that are allowed in C

module type IkindUnawareS = IntDomain_intf.IkindUnawareS

Interface of IntDomain implementations that do not take ikinds for arithmetic operations yet. TODO: Should be ported to S in the future.

module type S = IntDomain_intf.S

Interface of IntDomain implementations taking an ikind for arithmetic operations

module type SOverflow = IntDomain_intf.SOverflow

module type Y = IntDomain_intf.Y

The signature of integral value domains keeping track of ikind information

module type Z = IntDomain_intf.Z

module type Ikind = IntDomain_intf.Ikind

module type IntDomain = IntDomain_intf.IntDomain

module M = Messages

val (%) : ('a -> 'b) -> ('c -> 'a) -> 'c -> 'b

val (|?) : 'a option -> 'a -> 'a

exception IncompatibleIKinds of string

exception Unknown

exception Error

exception ArithmeticOnIntegerBot of string

type ana_int_config_values = {

mutable interval_threshold_widening : bool option;
mutable interval_narrow_by_meet : bool option;
mutable def_exc_widen_by_join : bool option;
mutable interval_threshold_widening_constants : string option;
mutable refinement : string option;

}

Define records that hold mutable variables representing different Configuration values. * These values are used to keep track of whether or not the corresponding Config values are en-/disabled

val ana_int_config : ana_int_config_values

val get_interval_threshold_widening : unit -> bool

val get_interval_narrow_by_meet : unit -> bool

val get_def_exc_widen_by_join : unit -> bool

val get_interval_threshold_widening_constants : unit -> string

val get_refinement : unit -> string

val should_wrap : GoblintCil.Cil.ikind -> bool

Whether for a given ikind, we should compute with wrap-around arithmetic. * Always for unsigned types, for signed types if 'sem.int.signed_overflow' is 'assume_wraparound'

val should_ignore_overflow : GoblintCil.Cil.ikind -> bool

Whether for a given ikind, we should assume there are no overflows. * Always false for unsigned types, true for signed types if 'sem.int.signed_overflow' is 'assume_none'

type overflow_info = IntDomain_intf.overflow_info = {

overflow : bool;
underflow : bool;

}

val set_overflow_flag : 
  cast:bool ->
  underflow:bool ->
  overflow:bool ->
  GoblintCil.Cil.ikind ->
  unit

val reset_lazy : unit -> unit

module type Bitfield_SOverflow = sig ... end

module IntDomLifter (I : S) : sig ... end

module PtrDiffIkind : Ikind

module IntDomWithDefaultIkind
  (I : Y)
  (Ik : Ikind) : 
  Y with type t = I.t and type int_t = I.int_t

module Size : sig ... end

module StdTop (B : sig ... end) : sig ... end

module Std (B : sig ... end) : sig ... end

module IntervalArith (Ints_t : IntOps.IntOps) : sig ... end

module IntInvariant : sig ... end

module SOverflowUnlifter
  (D : SOverflow) : 
  S with type int_t = D.int_t and type t = D.t

module IntIkind : sig ... end

module Integers
  (Ints_t : IntOps.IntOps) : 
  IkindUnawareS with type t = Ints_t.t and type int_t = Ints_t.t

module FlatPureIntegers : 
  IkindUnawareS with type t = int64 and type int_t = int64

module Flat
  (Base : IkindUnawareS) : 
  IkindUnawareS
    with type t = [ `Bot | `Lifted of Base.t | `Top ]
     and type int_t = Base.int_t

module Lift
  (Base : IkindUnawareS) : 
  IkindUnawareS
    with type t = [ `Bot | `Lifted of Base.t | `Top ]
     and type int_t = Base.int_t

module Flattened : sig ... end

module Lifted : sig ... end

module SOverflowLifter
  (D : S) : 
  SOverflow with type int_t = D.int_t and type t = D.t