Complete (frama-c-eva.Eva.Domain

Parameters

module Domain : InputDomain

Signature

val name : string

type context = unit

val context_dependencies : context Abstract_context.dependencies

val build_context : Domain.t -> context Eval.or_bottom

val backward_location : 
  Domain.t ->
  Eval.lval ->
  'loc ->
  'v ->
  ('loc * 'v) Eval.or_bottom

val reduce_further : Domain.t -> Eval.exp -> 'v -> (Eval.exp * 'v) list

val evaluate_predicate : 
  Domain.t Abstract_domain.logic_environment ->
  Domain.t ->
  Frama_c_kernel.Cil_types.predicate ->
  Frama_c_kernel.Abstract_interp.Comp.result

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

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

val enter_loop : Frama_c_kernel.Cil_types.stmt -> Domain.t -> Domain.t

val incr_loop_counter : Frama_c_kernel.Cil_types.stmt -> Domain.t -> Domain.t

val leave_loop : Frama_c_kernel.Cil_types.stmt -> Domain.t -> Domain.t

val project : Frama_c_kernel.Base.Hptset.t -> Domain.t -> Domain.t

val filter : Frama_c_kernel.Base.Hptset.t -> Domain.t -> Domain.t

val reuse : 
  Frama_c_kernel.Base.Hptset.t ->
  current_input:Domain.t ->
  previous_output:Domain.t ->
  Domain.t

val show_expr : 'a -> Domain.t -> Stdlib.Format.formatter -> Eval.exp -> unit

val post_analysis : Domain.t Frama_c_kernel.Lattice_bounds.or_bottom -> unit

module Store : sig ... end

val log_category : Eva__.Self.category

val key : Domain.t Abstract_domain.key