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.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.assigns -> unit) ->
Cil_types.kernel_function -> string -> unit
val fold_assigns :
(Emitter.t -> Cil_types.assigns -> 'a -> 'a) ->
Cil_types.kernel_function -> string -> 'a -> 'a
val iter_allocates :
(Emitter.t -> Cil_types.allocation -> unit) ->
Cil_types.kernel_function -> string -> unit
val fold_allocates :
(Emitter.t -> Cil_types.allocation -> 'a -> 'a) ->
Cil_types.kernel_function -> string -> 'a -> '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 -> 'a) ->
Cil_types.kernel_function -> string -> 'a -> 'a
val iter_behaviors :
(Emitter.t -> Cil_types.funbehavior -> unit) ->
Cil_types.kernel_function -> unit
val fold_behaviors :
(Emitter.t -> Cil_types.funbehavior -> '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.variant -> unit) ->
Cil_types.kernel_function -> unit
val fold_decreases :
(Emitter.t -> 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 -> unit
val add_check :
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 -> 'a -> unit
type 'a behavior_component_addition =
Emitter.t ->
Cil_types.kernel_function ->
?stmt:Cil_types.stmt ->
?active:string list -> ?behavior:string -> 'a -> 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.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.assigns Annotations.behavior_component_addition
val add_allocates :
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.allocation -> unit
val remove_assigns :
Emitter.t -> Cil_types.kernel_function -> 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) Stdlib.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)
Stdlib.ref
end