__ocaml_lex_comment_rec [Promelalexer_withexps] | |
__ocaml_lex_comment_rec [Promelalexer] | |
__ocaml_lex_comment_rec [Ltllexer] | |
__ocaml_lex_tables [Promelalexer_withexps] | |
__ocaml_lex_tables [Promelalexer] | |
__ocaml_lex_tables [Yalexer] | |
__ocaml_lex_tables [Ltllexer] | |
__ocaml_lex_token_rec [Promelalexer_withexps] | |
__ocaml_lex_token_rec [Promelalexer] | |
__ocaml_lex_token_rec [Yalexer] | |
__ocaml_lex_token_rec [Ltllexer] | |
A | |
abstract_logic_info [Data_for_aorai] |
Global logic info generated during type-checking (mostly encoding of
ghost variables having a logic type)
|
action_to_pred [Aorai_utils] |
for a given starting and ending state, returns the post-conditions
related to the possible values of the auxiliary variables at current point
the function, guarded by the fact that we have followed this path, from
the given program point
|
add [Path_analysis] | |
add_logic [Data_for_aorai] | |
add_offset [Utils_parser] | |
add_pre_post_from_buch [Aorai_visitors] | |
add_predicate [Data_for_aorai] | |
add_sync_with_buch [Aorai_visitors] | |
advance_abstract_interpretation [Aorai_option] | |
all_actions_preds [Aorai_utils] |
All actions that might have been performed on aux variables from the
given program point, guarded by the path followed.
|
aorai_assigns [Aorai_utils] |
returns assigns clause corresponding to updating automaton's state, and
assigning auxiliary variable depending on the possible transitions made
in the function.
|
at_most_one_path [Path_analysis] | |
auto_func_behaviors [Aorai_utils] |
auto_func_behaviors f st (st_status, tr_status)
generates behaviors corresponding to the transitions authorized by
tr_status for function f in status st
|
auto_func_block [Aorai_utils] | auto_func_block loc f status st res
generates the body of pre & post functions.
|
auto_func_preconditions [Aorai_utils] |
return list of preconditions for the given auxiliary function
(f_pre_func or f_post_func).
|
aux_variables [Data_for_aorai] |
Global auxiliary variables generated during type-checking of transitions
|
B | |
bool3_of_bool [Bool3] | |
bool3and [Bool3] | |
bool3not [Bool3] | |
bool3or [Bool3] | |
buf [Promelalexer_withexps] | |
buf [Promelalexer] | |
buf [Ltllexer] | |
C | |
c_file [Aorai_register] | |
clear [State_builder.Ref] |
Reset the reference to its default value.
|
comment [Promelalexer_withexps] | |
comment [Promelalexer] | |
comment [Ltllexer] | |
compute [Aorai_dataflow] | |
compute_ignored_functions [Aorai_visitors] | |
convert_ltl_exprs [Aorai_register] | |
copy [Datatype.S] |
Deep copy: no possible sharing between
x and copy x .
|
crosscond_to_pred [Aorai_utils] |
This function rewrites a cross condition into an ACSL expression.
|
D | |
dijkstra [Path_analysis] | |
display_status [Aorai_register] | |
dkey [Aorai_visitors] | |
dnfToCond [Logic_simplification] |
Given a DNF condition, it returns a condition in Promelaast.condition form.
|
dot_file [Aorai_register] | |
E | |
emitter [Aorai_option] |
The emitter which emits Aorai annotations.
|
empty [Path_analysis] | |
existing_path [Path_analysis] | |
extract_min [Path_analysis] | |
F | |
force_transition [Aorai_utils] |
returns the list of predicates expressing that for each current state
the automaton currently is in, there is at least one transition that is
crossed.
|
func_orig_table [Aorai_visitors] | |
G | |
generatesCFile [Aorai_register] | |
get [State_builder.Ref] |
Get the referenced value.
|
get_acceptance_pred [Aorai_visitors] | |
get_action_post_cond [Aorai_visitors] | |
get_call_name [Aorai_visitors] | |
get_edges [Path_analysis] | |
get_field_info_from_name [Utils_parser] | |
get_function_name [Parameter_sig.String] |
returns the given argument only if it is a valid function name
(see
Parameter_customize.get_c_ified_functions for more information),
and abort otherwise.
|
get_init_states [Path_analysis] | |
get_last_field [Utils_parser] | |
get_logic [Data_for_aorai] | |
get_new_offset [Utils_parser] | |
get_plain_string [Parameter_sig.String] |
always return the argument, even if the argument is not a function name.
|
get_possible_values [Parameter_sig.String] |
What are the acceptable values for this parameter.
|
get_predicate [Data_for_aorai] | |
get_preds_post_bc_wrt_params [Aorai_utils] | |
get_preds_pre_wrt_params [Aorai_utils] | |
get_range [Parameter_sig.Int] |
What is the possible range of values for this parameter.
|
get_transitions_of_state [Path_analysis] |
since Nitrogen-20111001
|
get_transitions_to_state [Path_analysis] | |
get_unchanged_aux_var [Aorai_visitors] | |
H | |
host_state_term [Aorai_utils] |
base lhost corresponding to curState.
|
I | |
incr [Parameter_sig.Int] |
Increment the integer.
|
initFile [Aorai_utils] |
Copy the file pointer locally in the class in order to easiest globals management and initializes some tables.
|
initGlobals [Aorai_utils] |
Given the name of the main function, this function computes all newly introduced globals (variables, enumeration structure, invariants, etc.)
|
init_file_names [Aorai_register] | |
init_test [Aorai_register] | |
isCrossable [Aorai_utils] |
Given a transition a function name and a function status (call or
return) it returns if the cross condition can be satisfied with
only function status.
|
isCrossableAtInit [Aorai_utils] |
Given a transition and the main entry point it returns if
the cross condition can be satisfied at the beginning of the program.
|
is_empty [Path_analysis] | |
is_on [Aorai_option] | |
is_out_of_state_exp [Aorai_utils] |
Returns the expression testing that automaton is NOT
in the corresponding state.
|
is_out_of_state_pred [Aorai_utils] |
Returns the predicate saying that automaton is NOT
in corresponding state.
|
is_out_of_state_stmt [Aorai_utils] |
Returns the statement saying the automaton is not in the corresponding
state.
|
is_state_exp [Aorai_utils] |
Returns the boolean expression saying the state is affected
|
is_state_pred [Aorai_utils] |
Returns the predicate saying that automaton is in
corresponding state.
|
is_state_stmt [Aorai_utils] |
Returns the statement saying the state is affected
|
K | |
kind_of_func [Aorai_visitors] | |
L | |
load_promela_file [Aorai_register] | |
load_promela_file_withexps [Aorai_register] | |
load_ya_file [Aorai_register] | |
loc [Promelalexer_withexps] | |
loc [Promelalexer] | |
loc [Yalexer] | |
loc [Ltllexer] | |
ltl [Ltlparser] | |
ltl2ba_params [Aorai_register] | |
ltl_file [Aorai_register] | |
ltl_tmp_file [Aorai_register] | |
ltl_to_ltlLight [Aorai_register] | |
ltl_to_promela [Aorai_register] | |
M | |
main [Aorai_register] | |
main [Yaparser] | |
make_enum_states [Aorai_utils] | |
make_type [Datatype.Hashtbl] | |
make_zero_one_choice [Aorai_visitors] | |
memo [Datatype.Hashtbl] | memo tbl k f returns the binding of k in tbl .
|
mk_auto_fct_block [Aorai_visitors] | |
mk_offseted_array [Aorai_utils] |
Given an lval term 'host' and an integer value 'off', it returns a lval term host
off .
|
mk_offseted_array_states_as_enum [Aorai_utils] |
Given an lval term 'host' and an integer value 'off', it returns a lval term host
off .
|
mk_post_fct_block [Aorai_visitors] | |
mk_pre_fct_block [Aorai_visitors] | |
mk_term_from_vi [Aorai_utils] |
Returns a term representing the given logic variable
(usually a fresh quantified variable).
|
N | |
needs_zero_one_choice [Aorai_visitors] | |
neg_trans [Aorai_visitors] | |
new_line [Yalexer] | |
newline [Promelalexer_withexps] | |
newline [Promelalexer] | |
newline [Ltllexer] | |
O | |
off [Parameter_sig.Bool] |
Set the boolean to
false .
|
on [Parameter_sig.Bool] |
Set the boolean to
true .
|
output [Aorai_register] | |
output [Ltl_output] | |
output_c_file [Aorai_register] | |
output_dot_automata [Promelaoutput] | |
P | |
parse [Promelalexer_withexps] | |
parse [Promelalexer] | |
parse [Yalexer] | |
parse [Ltllexer] | |
pebble_set_at [Data_for_aorai] |
Given a logic info representing a set of pebbles and a label, returns
the term corresponding to evaluating the set at the label.
|
possible_start [Aorai_visitors] | |
possible_states_preds [Aorai_utils] |
Returns a list of predicate giving for each possible start state the
disjunction of possible current states
|
post_treatment_loops [Aorai_visitors] | |
pred_reachable [Aorai_visitors] | |
print_action [Promelaoutput] | |
print_condition [Promelaoutput] | |
print_parsed [Promelaoutput] | |
print_parsed_condition [Promelaoutput] | |
print_parsed_expression [Promelaoutput] | |
print_raw_automata [Promelaoutput] | |
print_seq_elt [Promelaoutput] | |
print_sequence [Promelaoutput] | |
print_state [Promelaoutput] | |
print_statel [Promelaoutput] | |
print_transition [Promelaoutput] | |
print_transitionl [Promelaoutput] | |
printverb [Aorai_register] | |
promela [Promelaparser_withexps] | |
promela [Promelaparser] | |
promela_file [Aorai_register] | |
promela_file [Aorai_option] | |
R | |
raise_located [Promelalexer_withexps] | |
raise_located [Promelalexer] | |
raise_located [Yalexer] | |
raise_located [Ltllexer] | |
run [Aorai_register] | |
S | |
set [State_builder.Ref] |
Change the referenced value.
|
setCData [Data_for_aorai] |
Initializes some tables according to data from Cil AST.
|
set_ltl_correspondence [Aorai_register] | |
set_possible_values [Parameter_sig.String] |
Set what are the acceptable values for this parameter.
|
set_range [Parameter_sig.Int] |
Set what is the possible range of values for this parameter.
|
simplifyCond [Logic_simplification] |
Given a condition, this function does some logical simplifications
and returns an equivalent DNF form together with the simplified version
|
simplifyDNFwrtCtx [Logic_simplification] |
Given a DNF condition, it returns the same condition simplified according
to the context (function name and status).
|
simplifyTrans [Logic_simplification] |
Given a transition list, this function returns the same transition list with
simplifyCond done on each cross condition.
|
syntax_error [Aorai_register] | |
T | |
tand [Logic_simplification] |
smart constructors for typed conditions
|
test [Path_analysis] | |
tnot [Logic_simplification] | |
token [Promelalexer_withexps] | |
token [Promelalexer] | |
token [Yalexer] | |
token [Ltllexer] | |
tor [Logic_simplification] | |
U | |
update_loop_assigns [Aorai_visitors] | |
update_to_pred [Aorai_utils] |
Possible values of the given auxiliary variable under the current path,
start ing from the given point
|
V | |
voisins [Path_analysis] | |
W | |
work [Aorai_register] | |
Y | |
ya_file [Aorai_register] | |
Z | |
zero_term [Aorai_utils] |
Return an integer constant term with the 0 value.
|