Module LinearTwoVarEqualityDomain.D

include module type of struct include Printable.Std end

Default dummy definitions.

Include as the first thing to avoid these overriding actual definitions.

val tag : 'a -> 'b
val arbitrary : unit -> 'a
include sig ... end
val (*:) : Mpqf.t -> Mpqf.t -> Mpqf.t
val (+:) : Mpqf.t -> Mpqf.t -> Mpqf.t
val (-:) : Mpqf.t -> Mpqf.t -> Mpqf.t
val (/:) : Mpqf.t -> Mpqf.t -> Mpqf.t
val (=:) : Mpqf.t -> Mpqf.t -> Ppx_deriving_runtime.bool
val (<>:) : Mpqf.t -> Mpqf.t -> bool
val (<:) : Mpqf.t -> Mpqf.t -> bool
val (>:) : Mpqf.t -> Mpqf.t -> bool
val (<=:) : Mpqf.t -> Mpqf.t -> bool
val (>=:) : Mpqf.t -> Mpqf.t -> bool
val of_int : int -> Mpqf.t
include module type of struct include VarManagement end

VarManagement defines the type t of the affine equality domain (a record that contains an optional matrix and an apron environment) and provides the functions needed for handling variables (which are defined by RelationDomain.D2) such as add_vars, remove_vars. Furthermore, it provides the function simplified_monomials_from_texp that converts an apron expression into a list of monomials of reference variables and a constant offset

module EConj = VarManagement.EConj
include sig ... end
type t = {
  1. mutable d : EConj.t option;
  2. mutable env : GobApron.Environment.t;
}
val equal : t -> t -> Ppx_deriving_runtime.bool
val compare : t -> t -> Ppx_deriving_runtime.int
val hash : t -> int
val empty_env : GobApron.Environment.t
val bot : unit -> t
val get_env : t -> GobApron.Environment.t
val bot_env : t
val is_bot_env : t -> bool
val copy : t -> t
val change_d : t -> GobApron.Environment.t -> add:bool -> del:bool -> t
val vars : t -> Apron.Var.t list
val add_vars : t -> Apron.Var.t list -> t
val drop_vars : t -> Apron.Var.t list -> del:bool -> t
val remove_vars : t -> Apron.Var.t list -> t
val remove_vars_with : t -> Apron.Var.t list -> unit
val remove_filter : t -> (Apron.Var.t -> bool) -> t
val remove_filter_with : t -> (Apron.Var.t -> bool) -> unit
val keep_filter : t -> (Apron.Var.t -> bool) -> t
val keep_vars : t -> Apron.Var.t list -> t
val mem_var : t -> Apron.Var.t -> bool
val dim_add : Apron.Dim.change -> (EConj.IntMap.key * ((Z.t * EConj.IntMap.key) option * Z.t * Z.t) EConj.IntMap.t) -> EConj.IntMap.key * ((Z.t * EConj.IntMap.key) option * Z.t * Z.t) EConj.IntMap.t
val size : t -> int
val monomials_from_texp : t -> Apron.Texpr1.expr -> ((Goblint_std.GobZ.t * Apron.Dim.t) option * Goblint_std.GobZ.t * Goblint_std.GobZ.t) list option

Parses a Texpr to obtain a (coefficient, variable) pair list to repr. a sum of a variables that have a coefficient. If variable is None, the coefficient represents a constant offset.

val simplified_monomials_from_texp : t -> Apron.Texpr1.expr -> ((Z.t * Batteries.Int.t * Z.t) list * (Z.t * Z.t)) option
val simplify_to_ref_and_offset : t -> Apron.Texpr1.expr -> ((Z.t * Batteries.Int.t) option * Z.t * Z.t) option
module Bounds = ExpressionBounds
module V = RelationDomain.V
module Arg : sig ... end
module Convert : sig ... end
type var = V.t
val name : unit -> string
val to_yojson : 'a -> 'b
val is_bot : t -> Ppx_deriving_runtime.bool

t.d is some empty array and env is empty

val top_of : GobApron.Environment.t -> t

forall x_i in env, x_i:=X_i+0

val top : unit -> t

env = \emptyset, d = Some(||)

val is_top : t -> bool

is_top returns true for top_of array and empty array; precondition: t.env and t.d are of same size

val to_subscript : int -> string
val show_var : Apron.Environment.t -> Apron.Dim.t -> string
val show : t -> string

prints the current variable equalities with resolved variable names

val pretty : unit -> t -> GoblintCil.Pretty.doc
val printXml : 'a BatInnerIO.output -> t -> unit
val eval_interval : 'a -> Bounds.t -> Goblint_lib__.GobApron.Texpr1.t -> Z.t option * Z.t option
val meet_with_one_conj : t -> EConj.IntMap.key -> ((Z.t * Apron.Dim.t) option * Z.t * Z.t) -> t
val meet : t -> t -> t
val leq : t -> t -> bool
val join : t -> t -> t
val widen : t -> t -> t
val narrow : t -> t -> t
val pretty_diff : unit -> (t * t) -> GoblintCil.Pretty.doc
val forget_var : t -> Apron.Var.t -> t
val forget_vars : t -> Apron.Var.t list -> t
val assign_texpr : VarManagement.t -> Apron.Var.t -> Apron.Texpr1.expr -> t
val assign_exp : Queries.ask -> VarManagement.t -> Apron.Var.t -> GoblintCil.Cil.exp -> bool Stdlib.Lazy.t -> t
val assign_var : VarManagement.t -> Apron.Var.t -> Apron.Var.t -> t
val assign_var_parallel : t -> (Apron.Var.t * Apron.Var.t) list -> t
val assign_var_parallel_with : t -> (Apron.Var.t * Apron.Var.t) list -> unit
val assign_var_parallel' : t -> Apron.Var.t list -> Apron.Var.t list -> t
val substitute_exp : Queries.ask -> t -> Apron.Var.t -> GoblintCil.Cil.exp -> bool Stdlib.Lazy.t -> t
val meet_tcons : 'a -> t -> Apron.Tcons1.t -> GoblintCil.exp -> bool Stdlib.Lazy.t -> t
val unify : t -> t -> t
val assert_constraint : Queries.ask -> Bounds.t -> GoblintCil.Cil.exp -> bool -> bool Stdlib.Lazy.t -> t
val relift : 'a -> 'b
val invariant : t -> Apron.Lincons1.t list

representation as C expression

This function returns all the equalities that are saved in our datastructure t.

Lincons -> linear constraint

val cil_exp_of_lincons1 : GobApron.Lincons1.t -> GoblintCil.Cil.exp option
type marshal = t
val marshal : 'a -> 'b
val unmarshal : 'a -> 'b