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.