sig   val code_annot :     ?emitter:Emitter.t ->     ?filter:(Cil_types.code_annotation -> bool) ->     Cil_types.stmt -> Cil_types.code_annotation list   val code_annot_emitter :     ?filter:(Emitter.t -> Cil_types.code_annotation -> bool) ->     Cil_types.stmt -> (Cil_types.code_annotation * Emitter.t) list   exception No_funspec of Emitter.t   val funspec :     ?emitter:Emitter.t ->     ?populate:bool -> Cil_types.kernel_function -> Cil_types.funspec   val behaviors :     ?emitter:Emitter.t ->     ?populate:bool -> Cil_types.kernel_function -> Cil_types.funbehavior list   val decreases :     ?emitter:Emitter.t ->     ?populate:bool ->     Cil_types.kernel_function -> Cil_types.term Cil_types.variant option   val terminates :     ?emitter:Emitter.t ->     ?populate:bool ->     Cil_types.kernel_function -> Cil_types.identified_predicate option   val complete :     ?emitter:Emitter.t ->     ?populate:bool -> Cil_types.kernel_function -> string list list   val disjoint :     ?emitter:Emitter.t ->     ?populate:bool -> Cil_types.kernel_function -> string list list   val model_fields :     ?emitter:Emitter.t -> Cil_types.typ -> Cil_types.model_info list   val iter_code_annot :     (Emitter.t -> Cil_types.code_annotation -> unit) ->     Cil_types.stmt -> unit   val fold_code_annot :     (Emitter.t -> Cil_types.code_annotation -> '-> 'a) ->     Cil_types.stmt -> '-> 'a   val iter_all_code_annot :     ?sorted:bool ->     (Cil_types.stmt -> Emitter.t -> Cil_types.code_annotation -> unit) ->     unit   val fold_all_code_annot :     ?sorted:bool ->     (Cil_types.stmt -> Emitter.t -> Cil_types.code_annotation -> '-> 'a) ->     '-> 'a   val iter_global :     (Emitter.t -> Cil_types.global_annotation -> unit) -> unit   val fold_global :     (Emitter.t -> Cil_types.global_annotation -> '-> 'a) -> '-> 'a   val iter_requires :     (Emitter.t -> Cil_types.identified_predicate -> unit) ->     Cil_types.kernel_function -> string -> unit   val fold_requires :     (Emitter.t -> Cil_types.identified_predicate -> '-> 'a) ->     Cil_types.kernel_function -> string -> '-> 'a   val iter_assumes :     (Emitter.t -> Cil_types.identified_predicate -> unit) ->     Cil_types.kernel_function -> string -> unit   val fold_assumes :     (Emitter.t -> Cil_types.identified_predicate -> '-> 'a) ->     Cil_types.kernel_function -> string -> '-> 'a   val iter_ensures :     (Emitter.t ->      Cil_types.termination_kind * Cil_types.identified_predicate -> unit) ->     Cil_types.kernel_function -> string -> unit   val fold_ensures :     (Emitter.t ->      Cil_types.termination_kind * Cil_types.identified_predicate -> '-> 'a) ->     Cil_types.kernel_function -> string -> '-> 'a   val iter_assigns :     (Emitter.t -> Cil_types.identified_term Cil_types.assigns -> unit) ->     Cil_types.kernel_function -> string -> unit   val fold_assigns :     (Emitter.t -> Cil_types.identified_term Cil_types.assigns -> '-> 'a) ->     Cil_types.kernel_function -> string -> '-> 'a   val iter_allocates :     (Emitter.t -> Cil_types.identified_term Cil_types.allocation -> unit) ->     Cil_types.kernel_function -> string -> unit   val fold_allocates :     (Emitter.t -> Cil_types.identified_term Cil_types.allocation -> '-> 'a) ->     Cil_types.kernel_function -> string -> '-> 'a   val iter_extended :     (Emitter.t -> Cil_types.acsl_extension -> unit) ->     Cil_types.kernel_function -> string -> unit   val fold_extended :     (Emitter.t -> Cil_types.acsl_extension -> '-> 'a) ->     Cil_types.kernel_function -> string -> '-> 'a   val iter_behaviors :     (Emitter.t -> Cil_types.funbehavior -> unit) ->     Cil_types.kernel_function -> unit   val fold_behaviors :     (Emitter.t -> Cil_types.funbehavior -> '-> 'a) ->     Cil_types.kernel_function -> '-> 'a   val iter_complete :     (Emitter.t -> string list -> unit) -> Cil_types.kernel_function -> unit   val fold_complete :     (Emitter.t -> string list -> '-> 'a) ->     Cil_types.kernel_function -> '-> 'a   val iter_disjoint :     (Emitter.t -> string list -> unit) -> Cil_types.kernel_function -> unit   val fold_disjoint :     (Emitter.t -> string list -> '-> 'a) ->     Cil_types.kernel_function -> '-> 'a   val iter_terminates :     (Emitter.t -> Cil_types.identified_predicate -> unit) ->     Cil_types.kernel_function -> unit   val fold_terminates :     (Emitter.t -> Cil_types.identified_predicate -> '-> 'a) ->     Cil_types.kernel_function -> '-> 'a   val iter_decreases :     (Emitter.t -> Cil_types.term Cil_types.variant -> unit) ->     Cil_types.kernel_function -> unit   val fold_decreases :     (Emitter.t -> Cil_types.term Cil_types.variant -> '-> 'a) ->     Cil_types.kernel_function -> '-> 'a   val add_code_annot :     Emitter.t ->     ?kf:Cil_types.kernel_function ->     Cil_types.stmt -> Cil_types.code_annotation -> unit   val add_assert :     Emitter.t ->     ?kf:Cil_types.kernel_function ->     Cil_types.stmt -> Cil_types.predicate -> unit   val add_global : Emitter.t -> Cil_types.global_annotation -> unit   type 'a contract_component_addition =       Emitter.t ->       Cil_types.kernel_function ->       ?stmt:Cil_types.stmt -> ?active:string list -> '-> unit   type 'a behavior_component_addition =       Emitter.t ->       Cil_types.kernel_function ->       ?stmt:Cil_types.stmt ->       ?active:string list -> ?behavior:string -> '-> unit   val add_behaviors :     ?register_children:bool ->     Cil_types.funbehavior list Annotations.contract_component_addition   val add_decreases :     Emitter.t ->     Cil_types.kernel_function -> Cil_types.term Cil_types.variant -> unit   val add_terminates :     Cil_types.identified_predicate Annotations.contract_component_addition   val add_complete : string list Annotations.contract_component_addition   val add_disjoint : string list Annotations.contract_component_addition   val add_requires :     Cil_types.identified_predicate list     Annotations.behavior_component_addition   val add_assumes :     Cil_types.identified_predicate list     Annotations.behavior_component_addition   val add_ensures :     (Cil_types.termination_kind * Cil_types.identified_predicate) list     Annotations.behavior_component_addition   val add_assigns :     keep_empty:bool ->     Cil_types.identified_term Cil_types.assigns     Annotations.behavior_component_addition   val add_allocates :     Cil_types.identified_term Cil_types.allocation     Annotations.behavior_component_addition   val add_extended :     Cil_types.acsl_extension Annotations.behavior_component_addition   val remove_code_annot :     Emitter.t ->     ?kf:Cil_types.kernel_function ->     Cil_types.stmt -> Cil_types.code_annotation -> unit   val remove_global : Emitter.t -> Cil_types.global_annotation -> unit   val remove_behavior :     ?force:bool ->     Emitter.t -> Cil_types.kernel_function -> Cil_types.funbehavior -> unit   val remove_behavior_components :     Emitter.t -> Cil_types.kernel_function -> Cil_types.funbehavior -> unit   val remove_decreases : Emitter.t -> Cil_types.kernel_function -> unit   val remove_terminates : Emitter.t -> Cil_types.kernel_function -> unit   val remove_complete :     Emitter.t -> Cil_types.kernel_function -> string list -> unit   val remove_disjoint :     Emitter.t -> Cil_types.kernel_function -> string list -> unit   val remove_requires :     Emitter.t ->     Cil_types.kernel_function -> Cil_types.identified_predicate -> unit   val remove_assumes :     Emitter.t ->     Cil_types.kernel_function -> Cil_types.identified_predicate -> unit   val remove_ensures :     Emitter.t ->     Cil_types.kernel_function ->     Cil_types.termination_kind * Cil_types.identified_predicate -> unit   val remove_allocates :     Emitter.t ->     Cil_types.kernel_function ->     Cil_types.identified_term Cil_types.allocation -> unit   val remove_assigns :     Emitter.t ->     Cil_types.kernel_function ->     Cil_types.identified_term Cil_types.assigns -> unit   val remove_extended :     Emitter.t ->     Cil_types.kernel_function -> Cil_types.acsl_extension -> unit   val has_code_annot : ?emitter:Emitter.t -> Cil_types.stmt -> bool   val emitter_of_code_annot :     Cil_types.code_annotation -> Cil_types.stmt -> Emitter.t   val emitter_of_global : Cil_types.global_annotation -> Emitter.t   val logic_info_of_global : string -> Cil_types.logic_info list   val behavior_names_of_stmt_in_kf : Cil_types.kernel_function -> string list   val code_annot_of_kf :     Cil_types.kernel_function ->     (Cil_types.stmt * Cil_types.code_annotation) list   val fresh_behavior_name : Cil_types.kernel_function -> string -> string   val code_annot_state : State.t   val funspec_state : State.t   val global_state : State.t   val populate_spec_ref :     (Cil_types.kernel_function -> Cil_types.funspec -> bool) Pervasives.ref   val unsafe_add_global : Emitter.t -> Cil_types.global_annotation -> unit   val register_funspec :     ?emitter:Emitter.t -> ?force:bool -> Cil_types.kernel_function -> unit   val remove_alarm_ref :     (Emitter.Usable_emitter.t ->      Cil_types.stmt -> Cil_types.code_annotation -> unit)     Pervasives.ref end