Module E_ACSL.Translate_rtes

Generate and translate RTE annotations.

Translate the given RTE annotations into runtime checks in the given environment.