Index of values


D
do_all_rte [Dynamic_plugins.RteGen]
Generate all RTE annotations 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.

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
predicate_to_exp [Dynamic_plugins.E_ACSL]
print [Dynamic_plugins.Report]
print_csv [Dynamic_plugins.Report]
prover_of_name [Dynamic_plugins.Wp.Wpo]

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

W
wp_begin_session [Dynamic_plugins.Wp]
wp_clear [Dynamic_plugins.Wp]
wp_clear_session [Dynamic_plugins.Wp]
wp_compute [Dynamic_plugins.Wp]
wp_compute_call [Dynamic_plugins.Wp]
wp_compute_ip [Dynamic_plugins.Wp]
wp_compute_kf [Dynamic_plugins.Wp]
wp_end_session [Dynamic_plugins.Wp]
wp_iter_session [Dynamic_plugins.Wp]