SharedFunctions (goblint.Goblint

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 =

| Var_not_found of CilType.Varinfo.t
(*
Variable not found in Apron environment.
*)
| Cast_not_injective of CilType.Typ.t
(*
Cast is not injective, i.e. may under-/overflow.
*)
| Exp_not_supported
(*
Expression constructor not supported.
*)
| Overflow
(*
May overflow according to Apron bounds.
*)
| Exp_typeOf of exn
(*
Expression type could not be determined.
*)
| 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.

module ApronOfCil
  (V : SV)
  (Bounds : ConvBounds)
  (Arg : ConvertArg)
  (Tracked : RelationDomain.Tracked) : 
  sig ... end

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.

module Convert
  (V : SV)
  (Bounds : ConvBounds)
  (Arg : ConvertArg)
  (Tracked : RelationDomain.Tracked) : 
  sig ... end

Conversion between CIL expressions and Apron.

module type AbstractRelationalDomainRepresentation = sig ... end

module VarManagementOps
  (RelDomain : 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 Tracked : RelationDomain.Tracked

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

module Mpqf : sig ... end