Module ApronDomain.BoxProd0

Lift D to a non-reduced product with box. Both are updated in parallel, but D answers to queries. Box domain is used to filter out non-relational invariants for output.

Parameters

module D : S3

Signature

module BoxD : sig ... end
include sig ... end
val expand_fst : bool
val expand_snd : bool
type t = BoxD.t * D.t
val relift : t -> t
val tag : 'a -> 'b
val show : (BoxD.t * D.t) -> string
val name : unit -> string
val pretty : unit -> (BoxD.t * D.t) -> Printable.Pretty.doc
val printXml : 'a BatInnerIO.output -> (BoxD.t * D.t) -> unit
val to_yojson : (BoxD.t * D.t) -> [> `Assoc of (string * Yojson.Safe.t) list ]
val arbitrary : unit -> (BoxD.t * D.t) QCheck.arbitrary
val equal : ('a * D.t) -> ('b * D.t) -> bool
val hash : ('a * D.t) -> int
val compare : ('a * D.t) -> ('b * D.t) -> int
val leq : ('a * D.t) -> ('b * D.t) -> bool
val join : (BoxD.t * D.t) -> (BoxD.t * D.t) -> BoxD.t * D.t
val meet : (BoxD.t * D.t) -> (BoxD.t * D.t) -> BoxD.t * D.t
val widen : (BoxD.t * D.t) -> (BoxD.t * D.t) -> BoxD.t * D.t
val narrow : (BoxD.t * D.t) -> (BoxD.t * D.t) -> BoxD.t * D.t
val top : unit -> BoxD.t * D.t
val bot : unit -> BoxD.t * D.t
val is_top : ('a * D.t) -> bool
val is_bot : ('a * D.t) -> bool
val top_env : GobApron.Environment.t -> BoxD.Man.mt A.t * D.t
val bot_env : GobApron.Environment.t -> BoxD.Man.mt A.t * D.t
val is_top_env : ('a * D.t) -> bool
val is_bot_env : ('a * D.t) -> bool
val unify : (BoxD.t * D.t) -> (BoxD.t * D.t) -> BoxD.t * D.t
val copy : (BoxD.t * D.t) -> BoxD.t * D.t
type marshal = BoxD.marshal * D.marshal
val marshal : (BoxD.t * D.t) -> BoxD.marshal * D.marshal
val unmarshal : (BoxD.marshal * D.marshal) -> BoxD.t * D.t
val mem_var : ('a * D.t) -> GobApron.Var.t -> bool
val vars : ('a * D.t) -> GobApron.Var.t list
val pretty_diff : unit -> (('a * D.t) * ('b * D.t)) -> Lattice.Pretty.doc
val add_vars_with : (BoxD.Man.mt A.t * D.t) -> GobApron.Var.t list -> unit
val remove_vars_with : (BoxD.t * D.t) -> GobApron.Var.t list -> unit
val remove_filter_with : (BoxD.t * D.t) -> (GobApron.Var.t -> bool) -> unit
val keep_filter_with : (BoxD.Man.mt A.t * D.t) -> (GobApron.Var.t -> bool) -> unit
val keep_vars_with : (BoxD.Man.mt A.t * D.t) -> GobApron.Var.t list -> unit
val forget_vars_with : (BoxD.Man.mt A.t * D.t) -> GobApron.Var.t list -> unit
val assign_exp_with : Queries.ask -> (BoxD.Bounds.t * D.t) -> GobApron.Var.t -> GoblintCil.Cil.exp -> bool Stdlib.Lazy.t -> unit
val assign_exp_parallel_with : Queries.ask -> (BoxD.Man.mt A.t * D.t) -> (GobApron.Var.t * GoblintCil.exp) list -> bool -> unit
val assign_var_with : (BoxD.Man.mt A.t * D.t) -> GobApron.Var.t -> GobApron.Var.t -> unit
val assign_var_parallel_with : (BoxD.t * D.t) -> (GobApron.Var.t * GobApron.Var.t) list -> unit
val assign_var_parallel' : (BoxD.t * D.t) -> GobApron.Var.t list -> GobApron.Var.t list -> BoxD.t * D.t
val substitute_exp_with : Queries.ask -> (BoxD.Bounds.t * D.t) -> GobApron.Var.t -> GoblintCil.Cil.exp -> bool Stdlib.Lazy.t -> unit
val substitute_exp_parallel_with : Queries.ask -> (BoxD.Man.mt A.t * D.t) -> (GobApron.Var.t * GoblintCil.exp) list -> bool Stdlib.Lazy.t -> unit
val substitute_var_with : (BoxD.Man.mt A.t * D.t) -> GobApron.Var.t -> GobApron.Var.t -> unit
val meet_tcons : Queries.ask -> (BoxD.Man.mt A.t * D.t) -> GobApron.Tcons1.t -> GoblintCil.exp -> BoxD.Man.mt A.t * D.t
val to_lincons_array : ('a * D.t) -> GobApron.Lincons1.earray
val of_lincons_array : GobApron.Lincons1.earray -> BoxD.Man.mt A.t * D.t
val cil_exp_of_lincons1 : GobApron.Lincons1.t -> GoblintCil.exp option
val assert_inv : Queries.ask -> (BoxD.t * D.t) -> GoblintCil.exp -> bool -> bool Stdlib.Lazy.t -> BoxD.t * D.t
val eval_int : Queries.ask -> ('a * D.t) -> GoblintCil.exp -> bool Stdlib.Lazy.t -> ValueDomainQueries.ID.t
val invariant : (BoxD.Man.mt A.t * D.t) -> GobApron.Lincons1Set.elt list