Module Annotations

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 has_funspec : Cil_types.kernel_function -> bool
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 : ?⁠keep_empty:bool -> 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 contract_component_addition
val add_decreases : Emitter.t -> Cil_types.kernel_function -> Cil_types.variant -> unit
val add_terminates : Cil_types.identified_predicate contract_component_addition
val add_complete : string list contract_component_addition
val add_disjoint : string list contract_component_addition
val add_requires : Cil_types.identified_predicate list behavior_component_addition
val add_assumes : Cil_types.identified_predicate list behavior_component_addition
val add_ensures : (Cil_types.termination_kind * Cil_types.identified_predicate) list behavior_component_addition
val add_assigns : keep_empty:bool -> Cil_types.assigns behavior_component_addition
val add_allocates : keep_empty:bool -> Cil_types.allocation behavior_component_addition
val add_extended : Cil_types.acsl_extension 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