Up
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
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
]