module type LeafDomain =sig
..end
Part of an abstract domain signature automatically built by the
Domain_builder.Complete
functor. These functions can be redefined to achieve
better precision or performance. See Abstract_domain
for more details.
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