Module AffineEqualityDomain.D

Parameters

Signature

include module type of struct include Printable.Std end
val tag : 'a -> 'b
val arbitrary : unit -> 'a
include sig ... end
include sig ... end
module Vector : sig ... end
module Matrix : sig ... end
val dim_add : Apron.Dim.change -> Matrix.t -> Matrix.t
type t = {
  1. mutable d : AffineEqualityMatrix(Vc)(Mx).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 copy : t -> t
val dimchange2_add : t -> GobApron.Environment.t -> t
val dimchange2_remove : t -> GobApron.Environment.t -> t
val vars : t -> Apron.Var.t list
val add_vars : t -> Apron.Var.t list -> 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 (*:) : 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
val to_constant_opt : Vector.t -> Mpqf.t option
val get_coeff_vec : t -> Apron.Texpr1.expr -> Vector.t option
module Bounds : sig ... end
module V = RelationDomain.V
module Arg : sig ... end
module Convert : sig ... end
type var = V.t
val show : t -> string
val pretty : unit -> t -> GoblintCil.Pretty.doc
val printXml : 'a BatInnerIO.output -> t -> unit
val eval_interval : 'a -> Bounds.t -> GobApron.Texpr1.t -> Z.t option * Z.t option
val name : unit -> string
val to_yojson : 'a -> 'b
val is_bot : t -> Ppx_deriving_runtime.bool
val bot_env : t
val is_bot_env : t -> bool
val top : unit -> t
val is_top : t -> bool
val is_top_env : t -> bool
val meet : t -> t -> t
val leq : t -> t -> bool
val join : t -> t -> t
val widen : t -> t -> t
val narrow : 'a -> 'b -> 'a
val pretty_diff : unit -> (t * t) -> GoblintCil.Pretty.doc
val remove_rels_with_var : Matrix.t -> Apron.Var.t -> GobApron.Environment.t -> Matrix.t
val forget_vars : t -> Apron.Var.t list -> t
val assign_texpr : VarManagement(Vc)(Mx).t -> Apron.Var.t -> Apron.Texpr1.expr -> VarManagement(Vc)(Mx).t
val assign_exp : Queries.ask -> VarManagement(Vc)(Mx).t -> GobApron.Var.t -> GoblintCil.Cil.exp -> bool Stdlib.Lazy.t -> VarManagement(Vc)(Mx).t
val assign_var_parallel : t -> (Apron.Var.t * GobApron.Var.t) list -> t
val assign_var_parallel_with : t -> (Apron.Var.t * GobApron.Var.t) list -> unit
val assign_var_parallel' : t -> Apron.Var.t list -> GobApron.Var.t list -> t
val substitute_exp : Queries.ask -> t -> GobApron.Var.t -> GoblintCil.Cil.exp -> bool Stdlib.Lazy.t -> t

Assert a constraint expression.

The overflow is completely handled by the flag "no_ov", which is set in relationAnalysis.ml via the function no_overflow. In case of a potential overflow, "no_ov" is set to false and Convert.tcons1_of_cil_exp will raise the exception Unsupported_CilExp Overflow

val meet_tcons : 'a -> t -> GobApron.Tcons1.t -> 'b -> t
val unify : t -> t -> t
val assert_constraint : Queries.ask -> Bounds.t -> GoblintCil.exp -> bool -> bool Stdlib.Lazy.t -> t
val relift : 'a -> 'a
val invariant : t -> GobApron.Lincons1.t list
val cil_exp_of_lincons1 : GobApron.Lincons1.t -> GoblintCil.Cil.exp option
type marshal = t
val marshal : 'a -> 'a
val unmarshal : 'a -> 'a