Module Translate

module Translate: sig .. end
translate_* translates a given ACSL annotation into the corresponding C statement (if any) for runtime assertion checking. This C statements are part of the resulting environment.


translate_* translates a given ACSL annotation into the corresponding C statement (if any) for runtime assertion checking. This C statements are part of the resulting environment.
val translate_pre_spec : Cil_types.kernel_function -> Env.t -> Cil_types.funspec -> Env.t
val translate_post_spec : Cil_types.kernel_function -> Env.t -> Cil_types.funspec -> Env.t
val translate_pre_code_annotation : Cil_types.kernel_function -> Env.t -> Cil_types.code_annotation -> Env.t
val translate_post_code_annotation : Cil_types.kernel_function -> Env.t -> Cil_types.code_annotation -> Env.t
val translate_named_predicate : Cil_types.kernel_function -> Env.t -> Cil_types.predicate -> Env.t
val translate_rte_annots : (Format.formatter -> 'a -> unit) ->
'a ->
Cil_types.kernel_function -> Env.t -> Cil_types.code_annotation list -> Env.t
exception No_simple_translation of Cil_types.term
val term_to_exp : Cil_types.typ option -> Cil_types.term -> Cil_types.exp
val predicate_to_exp : Cil_types.kernel_function -> Cil_types.predicate -> Cil_types.exp