Index of values

D
do_all_rte [Dynamic_plugins.RteGen]

Generate all RTE annotations 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.

F
file_for_log_proof [Dynamic_plugins.Wp.Wpo]
force_run [Dynamic_plugins.Obfuscator]
G
generate_code [Dynamic_plugins.E_ACSL]
get_direct_component [Dynamic_plugins.Security_slicing]
get_forward_component [Dynamic_plugins.Security_slicing]
get_gid [Dynamic_plugins.Wp.Wpo]
get_indirect_backward_component [Dynamic_plugins.Security_slicing]
get_property [Dynamic_plugins.Wp.Wpo]
get_result [Dynamic_plugins.Wp.Wpo]
get_rte_annotations [Dynamic_plugins.RteGen]

Get the list of annotations previously emitted by RTE for the given statement.

goals_of_property [Dynamic_plugins.Wp.Wpo]
I
impact_analysis [Dynamic_plugins.Security_slicing]
is_valid [Dynamic_plugins.Wp.Wpo]
iter_on_goals [Dynamic_plugins.Wp.Wpo]
P
print [Dynamic_plugins.Report]
print_csv [Dynamic_plugins.Report]
prover_of_name [Dynamic_plugins.Wp.Wpo]
R
run [Dynamic_plugins.Aorai]
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.