Generate all RTE annotations in the given function.
Generate RTE annotations corresponding to -rte-precond in the given function.
The emitter used for generating RTE annotations
Generate RTE annotations corresponding to the given exp of the given stmt in the given function.
Get the list of annotations previously emitted by RTE for the given statement.
Create a .mli file used by 'make doc' to generate the html documentation of dynamic plug-ins.It takes the path where to create this file as an argument.
Generate RTE annotations corresponding to the given stmt of the given function.