Functor Domain_builder.Complete

module Complete: 
functor (Domain : InputDomain-> LeafDomain with type t := Domain.t

Automatically builds some functions of an abstract domain.

Parameters:
Domain : InputDomain

type t 
val backward_location : t ->
Cil_types.lval -> Cil_types.typ -> 'loc -> 'v -> ('loc * 'v) Eval.or_bottom
val reduce_further : t ->
Cil_types.exp -> 'v -> (Cil_types.exp * 'v) list
val evaluate_predicate : t Abstract_domain.logic_environment ->
t -> Cil_types.predicate -> Alarmset.status
val reduce_by_predicate : t Abstract_domain.logic_environment ->
t ->
Cil_types.predicate -> bool -> t Eval.or_bottom
val interpret_acsl_extension : Cil_types.acsl_extension ->
t Abstract_domain.logic_environment ->
t -> t
val enter_loop : Cil_types.stmt -> t -> t
val incr_loop_counter : Cil_types.stmt -> t -> t
val leave_loop : Cil_types.stmt -> t -> t
val filter : Cil_types.kernel_function ->
[ `Post | `Pre ] ->
Base.Hptset.t -> t -> t
val reuse : Cil_types.kernel_function ->
Base.Hptset.t ->
current_input:t ->
previous_output:t -> t
val show_expr : 'a ->
t ->
Stdlib.Format.formatter -> Cil_types.exp -> unit
val post_analysis : t Bottom.or_bottom -> unit
module Store: Domain_store.S  with type t := t
val key : t Abstract_domain.key