__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_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] | |
convert_ltl_exprs [Aorai_register] | |
copy [Datatype.S] | Deep copy: no possible sharing between |
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 |
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] | |
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 |
mk_offseted_array_states_as_enum [Aorai_utils] | Given an lval term 'host' and an integer value 'off', it returns a lval term host |
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 |
on [Parameter_sig.Bool] | Set the boolean to |
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,
|
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. |