Frama-C:
Plug-ins:
Libraries:

Frama-C API - LeafDomain

Part of an abstract domain signature automatically built by the Complete functor. These functions can be redefined to achieve better precision or performance. See Abstract_domain for more details.

type t
val name : string
type context = unit
val context_dependencies : context Abstract_context.dependencies
val build_context : t -> context Eval.or_bottom
val backward_location : t -> Eval.lval -> 'loc -> 'v -> ('loc * 'v) Eval.or_bottom
val reduce_further : t -> Eval.exp -> 'v -> (Eval.exp * 'v) list
val enter_loop : Frama_c_kernel.Cil_types.stmt -> t -> t
val incr_loop_counter : Frama_c_kernel.Cil_types.stmt -> t -> t
val leave_loop : Frama_c_kernel.Cil_types.stmt -> t -> t
val project : Frama_c_kernel.Base.Hptset.t -> t -> t
val filter : Frama_c_kernel.Base.Hptset.t -> t -> t
val reuse : Frama_c_kernel.Base.Hptset.t -> current_input:t -> previous_output:t -> t
val show_expr : 'a -> t -> Stdlib.Format.formatter -> Eval.exp -> unit
val post_analysis : t Frama_c_kernel.Lattice_bounds.or_bottom -> unit
module Store : Domain_store.S with type t := t
val log_category : Self.category