LeafDomain (frama-c-eva.Eva.Domain

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 evaluate_predicate : 
  t Abstract_domain.logic_environment ->
  t ->
  Frama_c_kernel.Cil_types.predicate ->
  Frama_c_kernel.Abstract_interp.Comp.result

val reduce_by_predicate : 
  t Abstract_domain.logic_environment ->
  t ->
  Frama_c_kernel.Cil_types.predicate ->
  bool ->
  t Eval.or_bottom

val interpret_acsl_extension : 
  Frama_c_kernel.Cil_types.acsl_extension ->
  t Abstract_domain.logic_environment ->
  t ->
  t

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 : sig ... end

val log_category : Eva__.Self.category

val key : t Abstract_domain.key