module ActiveBehaviors: sig
.. end
: Cil_types.behavior -> string
val pp_bhv : Format.formatter -> Cil_types.behavior -> unit
val is_active_aux : Cvalue.Model.t -> Cil_types.behavior -> Eval_terms.predicate_status
type
t = {
}
module HashBehaviors: Hashtbl.Make
(
sig
end
)
val create_from_spec : Cvalue.Model.t -> Cil_types.funspec -> t
val create : Cvalue.Model.t -> Cil_types.kernel_function -> t
val active : t ->
Cil_types.funbehavior -> Eval_terms.predicate_status
val is_active : t -> Cil_types.funbehavior -> bool
exception No_such_behavior
val behavior_from_name : t -> string -> Cil_types.behavior
val active_behaviors : t -> Cil_types.funbehavior list