Index of values

A
accept_base [Dynamic_plugins.Callgraph]

Returns true if the given base is a global, or a formal or local of either kf or one of its callers

all_statuses [Dynamic_plugins.RteGen]
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_in_rev_order [Dynamic_plugins.Callgraph]

Iterate over all the functions in the callgraph in reverse order

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
rm_asserts [Dynamic_plugins.Scope]

Remove redundant alarms.

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.