Index of values


__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]
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.