Module Goblint_lib.SharedFunctions

Relational value domain utilities.

module M = Messages
val int_of_scalar : ?scalewith:Z.t -> ?round:[< `Ceil | `Floor ] -> GobApron.Scalar.t -> Z.t option
module type ConvertArg = sig ... end
module type SV = RelationDomain.RV with type t = GobApron.Var.t
type unsupported_cilExp =
  1. | Var_not_found of CilType.Varinfo.t
    (*

    Variable not found in Apron environment.

    *)
  2. | Cast_not_injective of CilType.Typ.t
    (*

    Cast is not injective, i.e. may under-/overflow.

    *)
  3. | Exp_not_supported
    (*

    Expression constructor not supported.

    *)
  4. | Overflow
    (*

    May overflow according to Apron bounds.

    *)
  5. | Exp_typeOf of exn
    (*

    Expression type could not be determined.

    *)
  6. | BinOp_not_supported
    (*

    BinOp constructor not supported.

    *)
val pp_unsupported_cilExp : Ppx_deriving_runtime.Format.formatter -> unsupported_cilExp -> Ppx_deriving_runtime.unit
val show_unsupported_cilExp : unsupported_cilExp -> Ppx_deriving_runtime.string
module type ConvBounds = sig ... end

Interface for Bounds which calculates bounds for expressions and is used inside the - Convert module.

Conversion from CIL expressions to Apron. This is used by the domains "affine equalities" and "linear two variable equalities". It also handles the overflow through the flag "no_ov". For this reason it was divided from the Convert module for the pure apron domains "ApronOfCilForApronDomains",

module CilOfApron (V : SV) : sig ... end

Conversion from Apron to CIL expressions.

Conversion between CIL expressions and Apron.

module type AbstractRelationalDomainRepresentation = sig ... end
module type AssertionRelS = sig ... end

A more specific module type for RelationDomain.RelD2 with various apron elements. It is designed to be the interface for the D2 modules in affineEqualityDomain and apronDomain and serves as a functor argument for AssertionModule.

module AssertionModule (V : SV) (AD : AssertionRelS) (Arg : ConvertArg) : sig ... end
module Mpqf : sig ... end