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.
|