Frama-C API - Complete
Automatically builds some functions of an abstract domain.
Parameters
module Domain : InputDomainSignature
val context_dependencies : context Abstract_context.dependenciesval build_context : Domain.t -> context Eval.or_bottomval backward_location : Domain.t -> Eval.lval -> 'loc -> 'v -> ('loc * 'v) Eval.or_bottomval evaluate_predicate : Domain.t Abstract_domain.logic_environment -> Domain.t -> Frama_c_kernel.Cil_types.predicate -> Alarmset.statusval reduce_by_predicate : Domain.t Abstract_domain.logic_environment -> Domain.t -> Frama_c_kernel.Cil_types.predicate -> bool -> Domain.t Eval.or_bottomval interpret_acsl_extension : Frama_c_kernel.Cil_types.acsl_extension -> Domain.t Abstract_domain.logic_environment -> Domain.t -> Domain.tval enter_loop : Frama_c_kernel.Cil_types.stmt -> Domain.t -> Domain.tval incr_loop_counter : Frama_c_kernel.Cil_types.stmt -> Domain.t -> Domain.tval leave_loop : Frama_c_kernel.Cil_types.stmt -> Domain.t -> Domain.tval project : Frama_c_kernel.Base.Hptset.t -> Domain.t -> Domain.tval filter : Frama_c_kernel.Base.Hptset.t -> Domain.t -> Domain.tval reuse : Frama_c_kernel.Base.Hptset.t -> current_input:Domain.t -> previous_output:Domain.t -> Domain.tval post_analysis : Domain.t Frama_c_kernel.Lattice_bounds.or_bottom -> unitmodule Store : Domain_store.S with type t := Domain.tval log_category : Self.categoryval key : Domain.t Abstract_domain.key