Index of values


D
do_all_rte [Dynamic_plugins.RteGen]
Generate RTE annotations corresponding to -rte in the given function.
do_precond [Dynamic_plugins.RteGen]
Generate RTE annotations corresponding to -rte-precond in the given function.

E
emitter [Dynamic_plugins.RteGen]
The emitter used for generating RTE annotations
exp_annotations [Dynamic_plugins.RteGen]
Generate RTE annotations corresponding to the given exp of the given stmt in the given function.

G
get_rte_annotations [Dynamic_plugins.RteGen]
Get the list of annotations previously emitted by RTE for the given statement.

R
run [Dynamic_plugins.Print_api]
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.

S
stmt_annotations [Dynamic_plugins.RteGen]
Generate RTE annotations corresponding to the given stmt of the given function.