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