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.identified_predicate, Cil_types.identified_term)
Cil_types.behavior 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 -> 'a) ->
Cil_types.stmt -> 'a -> '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) ->
'a -> 'a
val iter_global :
(Emitter.t -> Cil_types.global_annotation -> unit) -> unit
val fold_global :
(Emitter.t -> Cil_types.global_annotation -> 'a -> 'a) -> '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 -> 'a) ->
Cil_types.kernel_function -> string -> 'a -> '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 -> 'a) ->
Cil_types.kernel_function -> string -> 'a -> '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 -> 'a) ->
Cil_types.kernel_function -> string -> 'a -> '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 -> 'a) ->
Cil_types.kernel_function -> string -> 'a -> '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 -> 'a) ->
Cil_types.kernel_function -> string -> 'a -> 'a
val iter_extended :
(Emitter.t -> string * int * Cil_types.identified_predicate list -> unit) ->
Cil_types.kernel_function -> string -> unit
val fold_extended :
(Emitter.t ->
string * int * Cil_types.identified_predicate list -> 'a -> 'a) ->
Cil_types.kernel_function -> string -> 'a -> 'a
val iter_behaviors :
(Emitter.t ->
(Cil_types.identified_predicate, Cil_types.identified_term)
Cil_types.behavior -> unit) ->
Cil_types.kernel_function -> unit
val fold_behaviors :
(Emitter.t ->
(Cil_types.identified_predicate, Cil_types.identified_term)
Cil_types.behavior -> 'a -> 'a) ->
Cil_types.kernel_function -> 'a -> 'a
val iter_complete :
(Emitter.t -> string list -> unit) -> Cil_types.kernel_function -> unit
val fold_complete :
(Emitter.t -> string list -> 'a -> 'a) ->
Cil_types.kernel_function -> 'a -> 'a
val iter_disjoint :
(Emitter.t -> string list -> unit) -> Cil_types.kernel_function -> unit
val fold_disjoint :
(Emitter.t -> string list -> 'a -> 'a) ->
Cil_types.kernel_function -> 'a -> '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 -> 'a) ->
Cil_types.kernel_function -> 'a -> '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 -> 'a) ->
Cil_types.kernel_function -> 'a -> '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 Cil_types.named -> unit
val add_global : Emitter.t -> Cil_types.global_annotation -> unit
val add_behaviors :
?register_children:bool ->
Emitter.t ->
Cil_types.kernel_function ->
(Cil_types.identified_predicate, Cil_types.identified_term)
Cil_types.behavior list -> unit
val add_decreases :
Emitter.t ->
Cil_types.kernel_function -> Cil_types.term Cil_types.variant -> unit
val add_terminates :
Emitter.t ->
Cil_types.kernel_function -> Cil_types.identified_predicate -> unit
val add_complete :
Emitter.t -> Cil_types.kernel_function -> string list -> unit
val add_disjoint :
Emitter.t -> Cil_types.kernel_function -> string list -> unit
val add_requires :
Emitter.t ->
Cil_types.kernel_function ->
string -> Cil_types.identified_predicate list -> unit
val add_assumes :
Emitter.t ->
Cil_types.kernel_function ->
string -> Cil_types.identified_predicate list -> unit
val add_ensures :
Emitter.t ->
Cil_types.kernel_function ->
string ->
(Cil_types.termination_kind * Cil_types.identified_predicate) list ->
unit
val add_assigns :
keep_empty:bool ->
Emitter.t ->
Cil_types.kernel_function ->
string -> Cil_types.identified_term Cil_types.assigns -> unit
val add_allocates :
Emitter.t ->
Cil_types.kernel_function ->
string -> Cil_types.identified_term Cil_types.allocation -> unit
val add_extended :
Emitter.t ->
Cil_types.kernel_function ->
string -> string * int * Cil_types.identified_predicate list -> unit
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.identified_predicate, Cil_types.identified_term)
Cil_types.behavior -> 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 ->
string * int * Cil_types.identified_predicate list -> 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