package goblint

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

Module IntDomain0

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 = {
  1. mutable interval_threshold_widening : bool option;
  2. mutable interval_narrow_by_meet : bool option;
  3. mutable def_exc_widen_by_join : bool option;
  4. mutable interval_threshold_widening_constants : string option;
  5. 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 = {
  1. overflow : bool;
  2. 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 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
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