Module Eval_annots.ActiveBehaviors

module ActiveBehaviors: sig .. end

val header : ('a, 'b) Cil_types.behavior -> string
val pp_bhv : Format.formatter -> ('a, 'b) Cil_types.behavior -> unit
val is_active_aux : Cvalue.Model.t ->
(Cil_types.identified_predicate, 'a) Cil_types.behavior ->
Eval_terms.predicate_status
type t = {
   init_state : Cvalue.Model.t;
   funspec : Cil_types.funspec;
   is_active : Cil_types.funbehavior -> Eval_terms.predicate_status;
}
module HashBehaviors: Hashtbl.Make(sig
type t = Cil_types.funbehavior 
val equal : ('a, 'b) Cil_types.behavior -> ('c, 'd) Cil_types.behavior -> bool
val hash : ('a, 'b) Cil_types.behavior -> int
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.identified_predicate, Cil_types.identified_term)
Cil_types.behavior
val active_behaviors : t -> Cil_types.funbehavior list