E_ACSL.Translate_rtes
Generate and translate RTE annotations.
val rte_annots :
(Stdlib.Format.formatter -> 'a -> unit) ->
'a ->
Frama_c_kernel.Cil_types.kernel_function ->
Env.t ->
Frama_c_kernel.Cil_types.code_annotation list ->
Env.t
Translate the given RTE annotations into runtime checks in the given environment.