sig   val header : 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 = {     init_state : Cvalue.Model.t;     funspec : Cil_types.funspec;     is_active : Cil_types.funbehavior -> Eval_terms.predicate_status;   }   module HashBehaviors :     sig       type key = Cil_types.funbehavior       type 'a t       val create : int -> 'a t       val clear : 'a t -> unit       val reset : 'a t -> unit       val copy : 'a t -> 'a t       val add : 'a t -> key -> '-> unit       val remove : 'a t -> key -> unit       val find : 'a t -> key -> 'a       val find_all : 'a t -> key -> 'a list       val replace : 'a t -> key -> '-> unit       val mem : 'a t -> key -> bool       val iter : (key -> '-> unit) -> 'a t -> unit       val filter_map_inplace : (key -> '-> 'a option) -> 'a t -> unit       val fold : (key -> '-> '-> 'b) -> 'a t -> '-> 'b       val length : 'a t -> int       val stats : 'a t -> Hashtbl.statistics     end   val create_from_spec :     Cvalue.Model.t -> Cil_types.funspec -> Eval_annots.ActiveBehaviors.t   val create :     Cvalue.Model.t ->     Cil_types.kernel_function -> Eval_annots.ActiveBehaviors.t   val active :     Eval_annots.ActiveBehaviors.t ->     Cil_types.funbehavior -> Eval_terms.predicate_status   val is_active :     Eval_annots.ActiveBehaviors.t -> Cil_types.funbehavior -> bool   exception No_such_behavior   val behavior_from_name :     Eval_annots.ActiveBehaviors.t -> string -> Cil_types.behavior   val active_behaviors :     Eval_annots.ActiveBehaviors.t -> Cil_types.funbehavior list end