| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1197 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (23 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (29 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (397 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (390 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (4 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (49 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (97 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (10 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (185 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (12 entries) |
Global Index
A
Aggregate [constructor, in values]And [constructor, in ast_basics]
anno [projection, in rt_validator]
annotation [projection, in rt_validator]
app_same_length_eq2 [lemma, in list_util]
app_same_length_eq [lemma, in list_util]
ArrayTypeDecl [constructor, in ast]
ArrayTypeDeclRT [constructor, in ast_rt]
arrayUpdate_with_typed_value_preserve_typed_array [lemma, in well_typed_util]
ArrayV [constructor, in values]
Array_Type [constructor, in ast_basics]
arrindex [definition, in ast_basics]
Assign [constructor, in ast]
AssignRT [constructor, in ast_rt]
ast [library]
astnum [definition, in ast_basics]
astNumber [projection, in rt_validator]
ast_number [projection, in rt_validator]
ast_util [library]
ast_rt [library]
ast_basics [library]
AuxiliaryFunctions [section, in ast]
AuxiliaryFunctions_For_AST_RT [section, in ast_util]
AuxiliaryFunctions_For_AST [section, in ast_util]
AuxiliaryFunctions_RT [section, in ast_rt]
B
beq_type_eq [lemma, in ast_basics]beq_type_refl [lemma, in ast_basics]
beq_type [definition, in ast_basics]
binary_operator [inductive, in ast_basics]
BinOp [constructor, in ast]
BinOpRT [constructor, in ast_rt]
binop_no_check_flagged_soundness [lemma, in rt_gen_consistent]
binop_no_check_soundness [lemma, in rt_gen_consistent]
binop_flagged_division_check_soundness [lemma, in rt_gen_consistent]
binop_division_check_soundness [lemma, in rt_gen_consistent]
binop_flagged_overflow_division_check_soundness [lemma, in rt_gen_consistent]
binop_overflow_division_check_soundness [lemma, in rt_gen_consistent]
binop_flagged_overflow_check_soundness [lemma, in rt_gen_consistent]
binop_overflow_check_soundness [lemma, in rt_gen_consistent]
binop_type [definition, in well_typed]
binop_arithm_operand_format [lemma, in eval_rt]
binop_logic_typed [lemma, in well_typed_util]
binop_arithm_typed [lemma, in well_typed_util]
binop_bool_type [lemma, in well_typed_util]
binop_int_type [lemma, in well_typed_util]
binop_int_operant_exists [lemma, in rt_opt_consistent_util]
Bool [constructor, in values]
Boolean [constructor, in ast_basics]
Boolean_Literal [constructor, in ast_basics]
Boolval [constructor, in values]
bound [inductive, in values]
bound_of_record_field_type_f_completeness [lemma, in rt_opt_impl_consistent]
bound_of_record_field_type_f_soundness [lemma, in rt_opt_impl_consistent]
bound_of_array_component_type_f_completeness [lemma, in rt_opt_impl_consistent]
bound_of_array_component_type_f_soundness [lemma, in rt_opt_impl_consistent]
bound_of_type_f_completeness [lemma, in rt_opt_impl_consistent]
bound_of_type_f_soundness [lemma, in rt_opt_impl_consistent]
C
Call [constructor, in ast]CallRT [constructor, in ast_rt]
CheckBinOpNil [constructor, in eval_rt]
ChecksBinOp [constructor, in eval_rt]
ChecksBinOpRTE [constructor, in eval_rt]
Checks_Generator_Implementation_Completeness_Proof [section, in rt_gen_impl_consistent]
Checks_Generator_Implementation_Soundness_Proof [section, in rt_gen_impl_consistent]
checks_validator [definition, in rt_validator]
Check_Count [section, in rt_counter]
check_flag_in_reserve2 [lemma, in rt_opt_util]
check_flag_in_reserve [lemma, in rt_opt_util]
check_flags [definition, in rt]
check_flag [inductive, in rt]
Check_Flags_Validator [section, in rt_validator]
cks_infor_t [record, in rt_counter]
cks_infor [constructor, in rt_counter]
col [projection, in symboltable]
copyIn [inductive, in eval]
copyInRT [inductive, in eval_rt]
copyInRT_completeness [lemma, in rt_gen_consistent]
copyInRT_soundness [lemma, in rt_gen_consistent]
CopyIn_Mode_Out_X [constructor, in eval_rt]
CopyIn_Mode_InOut_Range_X [constructor, in eval_rt]
CopyIn_Mode_InOut_Range_RTE_X [constructor, in eval_rt]
CopyIn_Mode_InOut_NoRange_X [constructor, in eval_rt]
CopyIn_Mode_InOut_eRTE_X [constructor, in eval_rt]
CopyIn_Mode_In_Range_X [constructor, in eval_rt]
CopyIn_Mode_In_Range_RTE_X [constructor, in eval_rt]
CopyIn_Mode_In_NoRangeCheck_X [constructor, in eval_rt]
CopyIn_Mode_In_eRTE_X [constructor, in eval_rt]
CopyIn_Nil_X [constructor, in eval_rt]
CopyIn_Mode_Out [constructor, in eval]
CopyIn_Mode_InOut_Range [constructor, in eval]
CopyIn_Mode_InOut_Range_RTE [constructor, in eval]
CopyIn_Mode_InOut_NoRange [constructor, in eval]
CopyIn_Mode_InOut_eRTE [constructor, in eval]
CopyIn_Mode_In_Range [constructor, in eval]
CopyIn_Mode_In_Range_RTE [constructor, in eval]
CopyIn_Mode_In_NoRange [constructor, in eval]
CopyIn_Mode_In_eRTE [constructor, in eval]
CopyIn_Nil [constructor, in eval]
copyOut [inductive, in eval]
copyOutRT [inductive, in eval_rt]
copyOutRT_completeness [lemma, in rt_gen_consistent]
copyOutRT_soundness [lemma, in rt_gen_consistent]
CopyOut_Mode_In_X [constructor, in eval_rt]
CopyOut_Mode_Out_Range_X [constructor, in eval_rt]
CopyOut_Mode_Out_Range_nRTE_X [constructor, in eval_rt]
CopyOut_Mode_Out_Range_RTE_X [constructor, in eval_rt]
CopyOut_Mode_Out_NoRange_X [constructor, in eval_rt]
CopyOut_Mode_Out_nRTE_X [constructor, in eval_rt]
CopyOut_Nil_X [constructor, in eval_rt]
CopyOut_Mode_In [constructor, in eval]
CopyOut_Mode_Out_Range [constructor, in eval]
CopyOut_Mode_Out_Range_nRTE [constructor, in eval]
CopyOut_Mode_Out_Range_RTE [constructor, in eval]
CopyOut_Mode_Out_NoRange [constructor, in eval]
CopyOut_Mode_Out_nRTE [constructor, in eval]
CopyOut_Nil [constructor, in eval]
copy_out_preserve_typed_stack [lemma, in well_typed_util]
copy_in_preserve_typed_store [lemma, in well_typed_util]
count_option_declaration_check_flags [definition, in rt_counter]
CpdtTactics [library]
cutUntil [inductive, in eval]
CutUntil_Tail [constructor, in eval]
CutUntil_Head [constructor, in eval]
CutUntil_Nil [constructor, in eval]
cut_until_preserve_typed_stack [lemma, in well_typed_util]
cut_until_uniqueness [lemma, in eval]
D
decl [inductive, in ast]declaration_astnum [projection, in ast]
declaration_astnum_rt [projection, in ast_rt]
declaration_ind [definition, in rt_gen_impl_consistent]
declaration_x_ind [definition, in rt_opt_impl_consistent]
declRT [inductive, in ast_rt]
decls [projection, in ast]
declsRT [projection, in ast_rt]
DerivedTypeDecl [constructor, in ast]
DerivedTypeDeclRT [constructor, in ast_rt]
Derived_Type [constructor, in ast_basics]
diff [constructor, in rt_validator]
diff_message' [record, in rt_validator]
diff_message [record, in rt_validator]
diff_annotation [inductive, in rt_validator]
diff' [constructor, in rt_validator]
DivByZero [constructor, in values]
DivCheck [constructor, in rt]
divCheck [inductive, in eval]
DivCheckBinop [constructor, in eval_rt]
DivCheck_M [constructor, in eval]
DivCheck_D [constructor, in eval]
DivCheck_RTE [constructor, in eval]
Divide [constructor, in ast_basics]
divide_result_in_bound_backward [lemma, in rt_opt_util]
divide_result_in_bound [lemma, in rt_opt_util]
divide_in_bound [lemma, in rt_opt_ZArith]
division_cks [projection, in rt_counter]
Division_Error [definition, in values]
DoCheckOnBinops [constructor, in eval]
DoCheckOnBinOp_Others [constructor, in eval]
DoCheckOnDivide [constructor, in eval]
DoCheckOnDivide_RTE [constructor, in eval]
DoCheckOnModulus [constructor, in eval]
DoCheckOnUnary_Minus [constructor, in eval]
DoCheckOnUnOp_Others [constructor, in eval]
done [definition, in CpdtTactics]
Do_Checks_Unop [constructor, in eval_rt]
Do_Checks_Unop_RTE [constructor, in eval_rt]
Do_Check_Unop_Nil [constructor, in eval_rt]
do_flagged_checks_on_plus_reserve [lemma, in rt_opt_util]
do_flagged_checks_on_modulus_reserve [lemma, in rt_opt_util]
do_flagged_checks_on_divide_reserve [lemma, in rt_opt_util]
do_range_check_same_result [lemma, in rt_opt_util]
do_range_checks_reserve [lemma, in rt_opt_util]
do_overflow_checks_reserve [lemma, in rt_opt_util]
do_run_time_check_on_unop [inductive, in eval]
do_run_time_check_on_binop [inductive, in eval]
E
endcol [projection, in symboltable]endline [projection, in symboltable]
ENTRY [module, in environment]
Entry_Value_Stored.T [definition, in eval]
Entry_Value_Stored [module, in eval]
ENTRY.T [axiom, in environment]
environment [library]
Equal [constructor, in ast_basics]
Error [constructor, in rt_validator]
errorType [inductive, in values]
Error' [constructor, in rt_validator]
eval [library]
EvalAssign [constructor, in eval]
EvalAssignRT [constructor, in eval_rt]
EvalAssignRT_Range [constructor, in eval_rt]
EvalAssignRT_Range_RTE [constructor, in eval_rt]
EvalAssignRT_RTE [constructor, in eval_rt]
EvalAssign_Range [constructor, in eval]
EvalAssign_Range_RTE [constructor, in eval]
EvalAssign_RTE [constructor, in eval]
EvalBinOp [constructor, in eval]
EvalBinOpE1_RTE [constructor, in eval]
EvalBinOpE2_RTE [constructor, in eval]
EvalBinOpRT [constructor, in eval_rt]
evalBinOpRT [inductive, in eval_rt]
EvalBinOpRTE1_RTE [constructor, in eval_rt]
EvalBinOpRTE2_RTE [constructor, in eval_rt]
evalBinOpRTS [inductive, in eval_rt]
EvalCall [constructor, in eval]
EvalCallRT [constructor, in eval_rt]
EvalCallRT_Body_RTE [constructor, in eval_rt]
EvalCallRT_Decl_RTE [constructor, in eval_rt]
EvalCallRT_Args_RTE [constructor, in eval_rt]
EvalCall_Body_RTE [constructor, in eval]
EvalCall_Decl_RTE [constructor, in eval]
EvalCall_Args_RTE [constructor, in eval]
evalDecl [inductive, in eval]
evalDeclRT [inductive, in eval_rt]
EvalDeclRT_Seq [constructor, in eval_rt]
EvalDeclRT_Seq_E [constructor, in eval_rt]
EvalDeclRT_Proc [constructor, in eval_rt]
EvalDeclRT_Type [constructor, in eval_rt]
EvalDeclRT_Var [constructor, in eval_rt]
EvalDeclRT_Var_Range_RTE [constructor, in eval_rt]
EvalDeclRT_Var_NoCheck [constructor, in eval_rt]
EvalDeclRT_Var_RTE [constructor, in eval_rt]
EvalDeclRT_Var_None [constructor, in eval_rt]
EvalDeclRT_Null [constructor, in eval_rt]
EvalDecl_Seq [constructor, in eval]
EvalDecl_Seq_RTE [constructor, in eval]
EvalDecl_Proc [constructor, in eval]
EvalDecl_Var_Range [constructor, in eval]
EvalDecl_Var_Range_RTE [constructor, in eval]
EvalDecl_Var [constructor, in eval]
EvalDecl_Var_RTE [constructor, in eval]
EvalDecl_Var_None [constructor, in eval]
EvalDecl_Type [constructor, in eval]
EvalDecl_Null [constructor, in eval]
evalExp [inductive, in eval]
evalExpRT [inductive, in eval_rt]
EvalIdentifier [constructor, in eval]
EvalIdentifierRT [constructor, in eval_rt]
EvalIfRT_False [constructor, in eval_rt]
EvalIfRT_True [constructor, in eval_rt]
EvalIfRT_RTE [constructor, in eval_rt]
EvalIf_False [constructor, in eval]
EvalIf_True [constructor, in eval]
EvalIf_RTE [constructor, in eval]
EvalIndexedComponent [constructor, in eval]
EvalIndexedComponentE_RTE [constructor, in eval]
EvalIndexedComponentRT [constructor, in eval_rt]
EvalIndexedComponentRTE_RTE [constructor, in eval_rt]
EvalIndexedComponentRTX_RTE [constructor, in eval_rt]
EvalIndexedComponentRT_Range_RTE [constructor, in eval_rt]
EvalIndexedComponentX_RTE [constructor, in eval]
EvalIndexedComponent_Range_RTE [constructor, in eval]
EvalLiteral [constructor, in eval]
evalLiteral [inductive, in eval]
EvalLiteralRT [constructor, in eval_rt]
evalLiteralRT [inductive, in eval_rt]
EvalLiteralRT_Int [constructor, in eval_rt]
EvalLiteralRT_Bool [constructor, in eval_rt]
EvalLiteral_Int [constructor, in eval]
EvalLiteral_Bool [constructor, in eval]
evalName [inductive, in eval]
EvalName [constructor, in eval]
evalNameRT [inductive, in eval_rt]
EvalNameRT [constructor, in eval_rt]
EvalNull [constructor, in eval]
EvalNullRT [constructor, in eval_rt]
EvalProgram [constructor, in eval]
evalProgram [inductive, in eval]
EvalProgramRT [constructor, in eval_rt]
evalProgramRT [inductive, in eval_rt]
EvalSelectedComponent [constructor, in eval]
EvalSelectedComponentRT [constructor, in eval_rt]
EvalSelectedComponentRTX_RTE [constructor, in eval_rt]
EvalSelectedComponentX_RTE [constructor, in eval]
EvalSeq [constructor, in eval]
EvalSeqRT [constructor, in eval_rt]
EvalSeqRT_RTE [constructor, in eval_rt]
EvalSeq_RTE [constructor, in eval]
evalStmt [inductive, in eval]
evalStmtRT [inductive, in eval_rt]
EvalUnOp [constructor, in eval]
EvalUnOpRT [constructor, in eval_rt]
evalUnOpRT [inductive, in eval_rt]
evalUnOpRTS [inductive, in eval_rt]
evalUnOpRTS_reserve [lemma, in rt_opt_util]
EvalUnOpRT_RTE [constructor, in eval_rt]
EvalUnOp_RTE [constructor, in eval]
EvalWhileRT_False [constructor, in eval_rt]
EvalWhileRT_True [constructor, in eval_rt]
EvalWhileRT_True_RTE [constructor, in eval_rt]
EvalWhileRT_RTE [constructor, in eval_rt]
EvalWhile_False [constructor, in eval]
EvalWhile_True [constructor, in eval]
EvalWhile_True_RTE [constructor, in eval]
EvalWhile_RTE [constructor, in eval]
eval_name_ex_cks_stripped [lemma, in eval_rt]
eval_exp_ex_cks_stripped [lemma, in eval_rt]
eval_name_ex_cks_added [lemma, in eval_rt]
eval_exp_ex_cks_added [lemma, in eval_rt]
eval_statement_preserve_typed_stack [lemma, in well_typed_util]
eval_declaration_preserve_typed_store [lemma, in well_typed_util]
eval_name_well_typed_value [lemma, in well_typed_util]
eval_expr_well_typed_value [lemma, in well_typed_util]
eval_expr_value_copy_out_opt_reserve_backward [lemma, in rt_opt_util]
eval_expr_value_copy_out_opt_reserve [lemma, in rt_opt_util]
eval_expr_value_reserve_backward [lemma, in rt_opt_util]
eval_expr_value_reserve [lemma, in rt_opt_util]
eval_name_value_in_bound' [lemma, in rt_opt_consistent_util]
eval_expr_value_in_bound' [lemma, in rt_opt_consistent_util]
eval_name_value_in_bound [lemma, in rt_opt_consistent_util]
eval_expr_value_in_bound [lemma, in rt_opt_consistent_util]
eval_rt [library]
exp [inductive, in ast]
expectedCompleteChecks [projection, in rt_validator]
expectedOptimizedChecks [projection, in rt_validator]
expected_complete_checks [projection, in rt_validator]
expected_optimized_checks [projection, in rt_validator]
expression_astnum [definition, in ast]
expression_ind [definition, in rt_gen_consistent]
expression_x_ind [definition, in eval_rt]
expression_ind [definition, in eval_rt]
expression_x_ind [definition, in rt_opt_consistent]
expression_ind [definition, in rt_opt_consistent]
expression_x_ind [definition, in rt_opt_util]
expression_ind [definition, in rt_opt_util]
expression_x_ind [definition, in rt_opt_consistent_util]
expression_ind [definition, in rt_opt_consistent_util]
expression_astnum_rt [definition, in ast_rt]
expression_ind [definition, in rt_gen_impl_consistent]
expression_x_ind [definition, in rt_opt_impl_consistent]
expRT [inductive, in ast_rt]
exp_exterior_checks_refl [lemma, in ast_util]
exp_updated_exterior_checks [lemma, in ast_util]
exp_type_same [lemma, in well_typed_util]
exp_exterior_checks_beq_nil [lemma, in rt_gen_util]
exp_ast_num_eq [lemma, in rt_gen_util]
exterior_checks [definition, in rt]
extract_subtype_range_unique [lemma, in symboltable]
extract_array_index_range_rt_unique [lemma, in symboltable]
Extract_Index_Range_RT [constructor, in symboltable]
extract_array_index_range_rt [inductive, in symboltable]
Extract_Range_RT [constructor, in symboltable]
extract_subtype_range_rt [inductive, in symboltable]
Extract_Index_Range [constructor, in symboltable]
extract_array_index_range [inductive, in symboltable]
Extract_Range [constructor, in symboltable]
extract_subtype_range [inductive, in symboltable]
extract_array_index_range_f_completeness [lemma, in rt_opt_impl_consistent]
extract_array_index_range_f_soundness [lemma, in rt_opt_impl_consistent]
extract_subtype_range_f_completeness [lemma, in rt_opt_impl_consistent]
extract_subtype_range_f_soundness [lemma, in rt_opt_impl_consistent]
F
fetchG_split [lemma, in well_typed_util]fetch_array_index_type_rt [definition, in symboltable]
fetch_array_index_type [definition, in symboltable]
fetch_sloc_rt [definition, in symboltable]
fetch_exp_type_rt [definition, in symboltable]
fetch_type_rt [definition, in symboltable]
fetch_proc_rt [definition, in symboltable]
fetch_var_rt [definition, in symboltable]
fetch_type_name_rt [definition, in symboltable]
fetch_pkg_name_rt [definition, in symboltable]
fetch_proc_name_rt [definition, in symboltable]
fetch_var_name_rt [definition, in symboltable]
fetch_sloc [definition, in symboltable]
fetch_exp_type [definition, in symboltable]
fetch_type [definition, in symboltable]
fetch_proc [definition, in symboltable]
fetch_var [definition, in symboltable]
fetch_type_name [definition, in symboltable]
fetch_pkg_name [definition, in symboltable]
fetch_proc_name [definition, in symboltable]
fetch_var_name [definition, in symboltable]
G
gnatproChecks [projection, in rt_validator]gnatpro_checks [projection, in rt_validator]
Greater_Than_Or_Equal [constructor, in ast_basics]
Greater_Than [constructor, in ast_basics]
H
half_modulus [definition, in values]I
IB_False [constructor, in values]IB_True [constructor, in values]
Identifier [constructor, in ast]
IdentifierRT [constructor, in ast_rt]
idnum [definition, in ast_basics]
If [constructor, in ast]
IfRT [constructor, in ast_rt]
In [constructor, in ast_basics]
IndexedComponent [constructor, in ast]
IndexedComponentRT [constructor, in ast_rt]
index_range_rel_backward [lemma, in rt_gen_util]
index_range_rel [lemma, in rt_gen_util]
initialization_exp [projection, in ast]
initialization_expRT [projection, in ast_rt]
Int [constructor, in values]
Integer [constructor, in ast_basics]
IntegerTypeDecl [constructor, in ast]
IntegerTypeDeclRT [constructor, in ast_rt]
Integer_Literal [constructor, in ast_basics]
Integer_Type [constructor, in ast_basics]
interior_checks [definition, in rt]
Interval [constructor, in values]
int32_bound [definition, in values]
In_Out [constructor, in ast_basics]
in_bound_unique [lemma, in rt_opt_util]
in_bound_value_neq_zero [lemma, in rt_opt_util]
In_Bound_Unary_Minus_Compat [lemma, in rt_opt_util]
In_Bound_Minus_Compat [lemma, in rt_opt_util]
In_Bound_Plus_Compat [lemma, in rt_opt_util]
In_Bound_Two [lemma, in rt_opt_util]
In_Bound_SubBound_Trans [lemma, in rt_opt_util]
In_Bound_Trans [lemma, in rt_opt_util]
in_bound_conflict [lemma, in rt_opt_util]
In_Bound_Refl [lemma, in rt_opt_util]
in_bound [inductive, in values]
in_bound_f_completeness [lemma, in rt_opt_impl_consistent]
in_bound_f_soundness [lemma, in rt_opt_impl_consistent]
is_in_out_mode [definition, in ast_basics]
is_out_mode [definition, in ast_basics]
is_in_mode [definition, in ast_basics]
is_range_constrainted_type [definition, in ast_basics]
L
LB_AuxiliaryFunctions [section, in ast_basics]leb_lt_false [lemma, in rt_opt_ZArith]
length_invcons [lemma, in list_util]
length_invnil [lemma, in list_util]
Less_Than_Or_Equal [constructor, in ast_basics]
Less_Than [constructor, in ast_basics]
level [definition, in symboltable]
le_max_rr [lemma, in rt_opt_ZArith]
le_max_rl [lemma, in rt_opt_ZArith]
le_max_lr [lemma, in rt_opt_ZArith]
le_max_ll [lemma, in rt_opt_ZArith]
le_min_rr [lemma, in rt_opt_ZArith]
le_min_rl [lemma, in rt_opt_ZArith]
le_min_lr [lemma, in rt_opt_ZArith]
le_min_ll [lemma, in rt_opt_ZArith]
Le_Neg_Ge [lemma, in rt_opt_ZArith]
Le_False_Lt [lemma, in rt_opt_ZArith]
line [projection, in symboltable]
list_util [library]
Literal [constructor, in ast]
literal [inductive, in ast_basics]
LiteralRT [constructor, in ast_rt]
literal_checks_optimization_soundness [lemma, in rt_opt_util]
Lte_Lt_Bool_False [lemma, in rt_opt_ZArith]
Lt_Neg_Gt [lemma, in rt_opt_ZArith]
Lt_False_Le [lemma, in rt_opt_ZArith]
Lt_Le_Bool_False [lemma, in rt_opt_ZArith]
M
main [projection, in ast]mainRT [projection, in ast_rt]
map_to_source_location [definition, in rt_validator]
Map_To_Source_Location [section, in rt_validator]
Math [module, in values]
Math.add [definition, in values]
Math.and [definition, in values]
Math.binary_operation [definition, in values]
Math.div [definition, in values]
Math.eq [definition, in values]
Math.ge [definition, in values]
Math.gt [definition, in values]
Math.le [definition, in values]
Math.lt [definition, in values]
Math.mod' [definition, in values]
Math.mul [definition, in values]
Math.ne [definition, in values]
Math.or [definition, in values]
Math.rem [definition, in values]
Math.sub [definition, in values]
Math.unary_operation [definition, in values]
Math.unary_minus [definition, in values]
Math.unary_plus [definition, in values]
Math.unary_not [definition, in values]
max_signed [definition, in values]
max_unsigned [definition, in values]
max_abs_f_ge0 [lemma, in rt_opt_ZArith]
max_abs_f_opp_le0 [lemma, in rt_opt_ZArith]
Minus [constructor, in ast_basics]
min_signed [definition, in values]
Mismatch [constructor, in rt_validator]
Mismatch' [constructor, in rt_validator]
mkNameTable [constructor, in symboltable_module]
mkobjDecl [constructor, in ast]
mkobjDeclRT [constructor, in ast_rt]
mkparamSpec [constructor, in ast]
mkparamSpecRT [constructor, in ast_rt]
mkprocBodyDecl [constructor, in ast]
mkprocBodyDeclRT [constructor, in ast_rt]
mkprogram [constructor, in ast]
mkprogramRT [constructor, in ast_rt]
mkSymTab [definition, in symboltable]
mkSymTabRT [definition, in symboltable]
mode [inductive, in ast_basics]
Modulus [constructor, in ast_basics]
modulus [definition, in values]
modulus_result_in_bound_backward [lemma, in rt_opt_util]
modulus_result_in_bound [lemma, in rt_opt_util]
modulus_in_bound_trans [lemma, in rt_opt_util]
modulus_in_int32_bound [lemma, in rt_opt_util]
modulus_in_bound [lemma, in rt_opt_ZArith]
Multiply [constructor, in ast_basics]
multiply_in_bound [lemma, in rt_opt_ZArith]
N
name [inductive, in ast]Name [constructor, in ast]
nameRT [inductive, in ast_rt]
NameRT [constructor, in ast_rt]
nametable [record, in symboltable_module]
name_astnum [definition, in ast]
name_exterior_checks_refl [lemma, in ast_util]
name_updated_exterior_checks [lemma, in ast_util]
name_ind [definition, in rt_gen_consistent]
name_x_ind [definition, in eval_rt]
name_ind [definition, in eval_rt]
name_x_ind [definition, in rt_opt_consistent]
name_ind [definition, in rt_opt_consistent]
name_x_ind [definition, in rt_opt_util]
name_ind [definition, in rt_opt_util]
name_x_ind [definition, in rt_opt_consistent_util]
name_ind [definition, in rt_opt_consistent_util]
name_astnum_rt [definition, in ast_rt]
name_ind [definition, in rt_gen_impl_consistent]
name_exterior_checks_beq_nil [lemma, in rt_gen_util]
name_ast_num_eq [lemma, in rt_gen_util]
name_x_ind [definition, in rt_opt_impl_consistent]
Not [constructor, in ast_basics]
Not_Equal [constructor, in ast_basics]
not_inbetween_opt_cmp_cks [constructor, in rt_validator]
not_subset_of_cmp_cks [constructor, in rt_validator]
not_superset_of_opt_cks [constructor, in rt_validator]
Null [constructor, in ast]
NullDecl [constructor, in ast]
NullDeclRT [constructor, in ast_rt]
NullRT [constructor, in ast_rt]
num_of_cks [projection, in rt_counter]
O
ObjDecl [constructor, in ast]objDecl [record, in ast]
ObjDeclRT [constructor, in ast_rt]
objDeclRT [record, in ast_rt]
object_nominal_subtype [projection, in ast]
object_name [projection, in ast]
object_nominal_subtype_rt [projection, in ast_rt]
object_nameRT [projection, in ast_rt]
OK [constructor, in values]
OK [constructor, in rt_validator]
OK' [constructor, in rt_validator]
optArgsImpl_completeness [lemma, in rt_opt_impl_consistent]
optArgsImpl_soundness [lemma, in rt_opt_impl_consistent]
optArgs_copyout_completeness [lemma, in rt_opt_consistent]
optArgs_copyout_soundness [lemma, in rt_opt_consistent]
optArgs_copyin_soundness' [lemma, in rt_opt_consistent_util]
optArgs_copyin_completeness' [lemma, in rt_opt_consistent_util]
optArgs_copyin_completeness [lemma, in rt_opt_consistent_util]
optArgs_copyin_soundness [lemma, in rt_opt_consistent_util]
optDeclConsistent [lemma, in rt_opt_consistent]
optDeclImplConsistent [lemma, in rt_opt_impl_consistent]
optDeclImpl_completeness [lemma, in rt_opt_impl_consistent]
optDeclImpl_soundness [lemma, in rt_opt_impl_consistent]
optDecl_completeness [lemma, in rt_opt_consistent]
optDecl_soundness [lemma, in rt_opt_consistent]
optExpConsistent [lemma, in rt_opt_consistent]
optExpImplConsistent [lemma, in rt_opt_impl_consistent]
optExpImpl_completeness [lemma, in rt_opt_impl_consistent]
optExpImpl_soundness [lemma, in rt_opt_impl_consistent]
optExp_soundness' [lemma, in rt_opt_consistent_util]
optExp_completeness' [lemma, in rt_opt_consistent_util]
optExp_completeness [lemma, in rt_opt_consistent_util]
optExp_soundness [lemma, in rt_opt_consistent_util]
optimize_name_ex_cks_stripped [lemma, in rt_opt_util]
optimize_exp_ex_cks_stripped [lemma, in rt_opt_util]
optimize_range_check_on_copy_out_reserve [lemma, in rt_opt_util]
optimize_range_check_reserve [lemma, in rt_opt_util]
optimize_overflow_check_reserve [lemma, in rt_opt_util]
optimize_range_check_backward [lemma, in rt_opt_util]
optimize_range_check_preserve_backward [lemma, in rt_opt_util]
optimize_range_check_preserve [lemma, in rt_opt_util]
optimize_name_ex_cks_eq [lemma, in rt_opt_util]
optimize_exp_ex_cks_eq [lemma, in rt_opt_util]
optimize_name_ast_num_eq [lemma, in rt_opt_util]
optimize_name_exist_int_value [lemma, in rt_opt_consistent_util]
optimize_expression_exist_int_value [lemma, in rt_opt_consistent_util]
optimize_range_check_both_reserve_storeUpdate_backward [lemma, in rt_opt_consistent_util]
optimize_range_check_both_reserve_storeUpdate [lemma, in rt_opt_consistent_util]
optimize_range_check_on_copy_out_reserve_storeUpdate_backward [lemma, in rt_opt_consistent_util]
optimize_range_check_on_copy_out_reserve_storeUpdate [lemma, in rt_opt_consistent_util]
optimize_range_check_reserve_storeUpdate_backward [lemma, in rt_opt_consistent_util]
optimize_range_check_reserve_storeUpdate [lemma, in rt_opt_consistent_util]
optimize_rtc_unop_f_completeness [lemma, in rt_opt_impl_consistent]
optimize_rtc_unop_f_soundness [lemma, in rt_opt_impl_consistent]
optimize_rtc_binop_f_completeness [lemma, in rt_opt_impl_consistent]
optimize_rtc_binop_f_soundness [lemma, in rt_opt_impl_consistent]
optimize_range_check_on_copy_out_f_completeness [lemma, in rt_opt_impl_consistent]
optimize_range_check_on_copy_out_f_soundness [lemma, in rt_opt_impl_consistent]
optimize_range_check_f_completeness [lemma, in rt_opt_impl_consistent]
optimize_range_check_f_soundness [lemma, in rt_opt_impl_consistent]
optimize_overflow_check_f_completeness [lemma, in rt_opt_impl_consistent]
optimize_overflow_check_f_soundness [lemma, in rt_opt_impl_consistent]
optLiteralImpl_completeness [lemma, in rt_opt_impl_consistent]
optLiteralImpl_soundness [lemma, in rt_opt_impl_consistent]
optNameImplConsistent [lemma, in rt_opt_impl_consistent]
optNameImpl_completeness [lemma, in rt_opt_impl_consistent]
optNameImpl_soundness [lemma, in rt_opt_impl_consistent]
optName_soundness' [lemma, in rt_opt_consistent_util]
optName_completeness' [lemma, in rt_opt_consistent_util]
optName_completeness [lemma, in rt_opt_consistent_util]
optName_soundness [lemma, in rt_opt_consistent_util]
optObjDeclImpl_completeness [lemma, in rt_opt_impl_consistent]
optObjDeclImpl_soundness [lemma, in rt_opt_impl_consistent]
optProgramConsistent [lemma, in rt_opt_consistent]
optProgramImplConsistent [lemma, in rt_opt_impl_consistent]
optProgramImpl_completeness [lemma, in rt_opt_impl_consistent]
optProgramImpl_soundness [lemma, in rt_opt_impl_consistent]
optProgram_completeness [lemma, in rt_opt_consistent]
optProgram_soundness [lemma, in rt_opt_consistent]
optStmtConsistent [lemma, in rt_opt_consistent]
optStmtImplConsistent [lemma, in rt_opt_impl_consistent]
optStmtImpl_completeness [lemma, in rt_opt_impl_consistent]
optStmtImpl_soundness [lemma, in rt_opt_impl_consistent]
optStmt_completeness [lemma, in rt_opt_consistent]
optStmt_soundness [lemma, in rt_opt_consistent]
Or [constructor, in ast_basics]
Out [constructor, in ast_basics]
OverflowCheck [constructor, in rt]
overflowCheck [inductive, in eval]
OverflowCheckBinop [constructor, in eval_rt]
overflowChecks [inductive, in eval_rt]
OverflowCheckUnop [constructor, in eval_rt]
OverflowCheck_List [constructor, in eval_rt]
OverflowCheck_Nil [constructor, in eval_rt]
OverflowCheck_OK [constructor, in eval]
OverflowCheck_Fail [constructor, in eval]
OverflowError [constructor, in values]
overflow_check_OK_exist_int [lemma, in rt_gen_consistent]
overflow_cks [projection, in rt_counter]
Overflow_Error [definition, in values]
P
parameter_mode [projection, in ast]parameter_subtype_mark [projection, in ast]
parameter_name [projection, in ast]
parameter_astnum [projection, in ast]
parameter_mode_rt [projection, in ast_rt]
parameter_subtype_mark_rt [projection, in ast_rt]
parameter_nameRT [projection, in ast_rt]
parameter_astnum_rt [projection, in ast_rt]
paramSpec [record, in ast]
paramSpecRT [record, in ast_rt]
pkgNames [projection, in symboltable_module]
pkgnum [definition, in ast_basics]
Plus [constructor, in ast_basics]
plus_result_in_bound_backward [lemma, in rt_opt_util]
plus_result_in_bound [lemma, in rt_opt_util]
procBodyDecl [inductive, in ast]
ProcBodyDecl [constructor, in ast]
procBodyDeclRT [inductive, in ast_rt]
ProcBodyDeclRT [constructor, in ast_rt]
procedure_name [definition, in ast]
procedure_parameter_profile [definition, in ast]
procedure_declarative_part [definition, in ast]
procedure_statements [definition, in ast]
procedure_parameter_profile_rt [definition, in ast_rt]
procedure_declarative_part_rt [definition, in ast_rt]
procedure_statements_rt [definition, in ast_rt]
procedure_body_ind [definition, in rt_gen_impl_consistent]
procedure_declaration_rel_backward [lemma, in rt_gen_util]
procedure_declaration_rel [lemma, in rt_gen_util]
procedure_components_rel [lemma, in rt_gen_util]
procedure_body_x_ind [definition, in rt_opt_impl_consistent]
procedur_name_rt [definition, in ast_rt]
procNames [projection, in symboltable_module]
procnum [definition, in ast_basics]
proc_decl_rt [definition, in symboltable]
proc_decl [definition, in symboltable]
program [record, in ast]
programRT [record, in ast_rt]
program_checks_validator [definition, in rt_validator]
push_typed_value_preserve_typed_store [lemma, in well_typed_util]
push_value_in_range_preserve_typed_store [lemma, in well_typed_util]
R
Range [constructor, in ast]range [inductive, in ast]
RangeCheck [constructor, in rt]
rangeCheck [inductive, in eval]
RangeCheckOnReturn [constructor, in rt]
rangeChecks [inductive, in eval_rt]
RangeCheck_List [constructor, in eval_rt]
RangeCheck_Nil [constructor, in eval_rt]
RangeCheck_OK [constructor, in eval]
RangeCheck_Fail [constructor, in eval]
RangeError [constructor, in values]
RangeRT [constructor, in ast_rt]
rangeRT [inductive, in ast_rt]
range_constrainted_type_true [lemma, in well_typed_util]
range_cks [projection, in rt_counter]
range_check_opt_subBound_true [lemma, in rt_opt_util]
range_check_on_copyout_preserve [lemma, in rt_opt_util]
Range_Error [definition, in values]
range_constrainted_type_true [lemma, in rt_opt_impl_consistent]
RecordTypeDecl [constructor, in ast]
RecordTypeDeclRT [constructor, in ast_rt]
recordUpdate_with_typed_value_preserve_typed_array [lemma, in well_typed_util]
RecordV [constructor, in values]
Record_Type [constructor, in ast_basics]
removed_check_flag_notin [lemma, in rt_opt_util]
remove_check_on_unop_reserve [lemma, in rt_opt_util]
remove_check_on_binop_reserve [lemma, in rt_opt_util]
remove_notin_check_flag [lemma, in rt_opt_util]
reside_symtable_sloc_rt [definition, in symboltable]
reside_symtable_exps_rt [definition, in symboltable]
reside_symtable_types_rt [definition, in symboltable]
reside_symtable_procs_rt [definition, in symboltable]
reside_symtable_vars_rt [definition, in symboltable]
reside_nametable_types_rt [definition, in symboltable]
reside_nametable_pkgs_rt [definition, in symboltable]
reside_nametable_procs_rt [definition, in symboltable]
reside_nametable_vars_rt [definition, in symboltable]
reside_symtable_sloc [definition, in symboltable]
reside_symtable_exps [definition, in symboltable]
reside_symtable_types [definition, in symboltable]
reside_symtable_procs [definition, in symboltable]
reside_symtable_vars [definition, in symboltable]
reside_nametable_types [definition, in symboltable]
reside_nametable_pkgs [definition, in symboltable]
reside_nametable_procs [definition, in symboltable]
reside_nametable_vars [definition, in symboltable]
Ret [inductive, in values]
return_message' [inductive, in rt_validator]
return_message [inductive, in rt_validator]
rt [library]
RTE [constructor, in values]
rt_gen_util [library]
rt_validator [library]
rt_opt [library]
rt_gen [library]
rt_counter [library]
rt_opt_consistent [library]
rt_opt_consistent_util [library]
rt_opt_impl [library]
rt_opt_util [library]
rt_gen_consistent [library]
rt_opt_ZArith [library]
rt_gen_impl [library]
rt_opt_impl_consistent [library]
rt_gen_impl_consistent [library]
S
safe_remove_unop_check [lemma, in rt_opt_util]safe_remove_binop_check [lemma, in rt_opt_util]
SelectedComponent [constructor, in ast]
SelectedComponentRT [constructor, in ast_rt]
Seq [constructor, in ast]
SeqDecl [constructor, in ast]
SeqDeclRT [constructor, in ast_rt]
SeqRT [constructor, in ast_rt]
sloc [constructor, in symboltable]
sourceLoc [projection, in rt_validator]
source_location [record, in symboltable]
split1_complete [lemma, in list_util]
split1_correct_length [lemma, in list_util]
split1_correct_eq [lemma, in list_util]
split1_correct [lemma, in list_util]
split2_complete [lemma, in list_util]
split2_length_ok [lemma, in list_util]
split2_correct [lemma, in list_util]
split2_equation3 [lemma, in list_util]
split2_equation2 [lemma, in list_util]
split2_equation1 [lemma, in list_util]
STACK [module, in eval]
stmt [inductive, in ast]
stmtRT [inductive, in ast_rt]
STORE [module, in environment]
storeUpdate [inductive, in eval]
storeUpdateRT [inductive, in eval_rt]
storeUpdateRT_completeness [lemma, in rt_gen_consistent]
storeUpdateRT_soundness [lemma, in rt_gen_consistent]
storeUpdateRT_opt_soundness' [lemma, in rt_opt_consistent_util]
storeUpdateRT_opt_completeness' [lemma, in rt_opt_consistent_util]
storeUpdateRT_opt_completeness [lemma, in rt_opt_consistent_util]
storeUpdateRT_opt_soundness [lemma, in rt_opt_consistent_util]
storeUpdate_with_typed_value_preserve_typed_stack [lemma, in well_typed_util]
storeUpdate_with_typed_value_preserve_typed_store [lemma, in well_typed_util]
store_update_ex_cks_stripped [lemma, in eval_rt]
store_update_ex_cks_added [lemma, in eval_rt]
STORE.cut_to [definition, in environment]
STORE.eqncons [constructor, in environment]
STORE.eqnil [constructor, in environment]
STORE.fetch [definition, in environment]
STORE.frame [definition, in environment]
STORE.level_of [definition, in environment]
STORE.newFrame [definition, in environment]
STORE.push [definition, in environment]
STORE.pushG [definition, in environment]
STORE.reside [definition, in environment]
STORE.scope_level [definition, in environment]
STORE.stack_eq_length_trans2 [lemma, in environment]
STORE.stack_eq_length_trans [lemma, in environment]
STORE.stack_eq_length_sym [lemma, in environment]
STORE.stack_eq_length_refl2 [lemma, in environment]
STORE.stack_eq_length_refl [lemma, in environment]
STORE.stack_eq_length [inductive, in environment]
STORE.state [definition, in environment]
STORE.store [definition, in environment]
STORE.store_of [definition, in environment]
STORE.update [definition, in environment]
STORE.updateG_length [lemma, in environment]
STORE.updates_length [lemma, in environment]
STORE.V [abbreviation, in environment]
Subtype [constructor, in ast_basics]
SubtypeDecl [constructor, in ast]
SubtypeDeclRT [constructor, in ast_rt]
subtype_range [definition, in ast]
subtype_num [definition, in ast_basics]
subtype_range_rt [definition, in ast_rt]
subtype_range_rel_backward [lemma, in rt_gen_util]
subtype_range_rel [lemma, in rt_gen_util]
sub_bound_unique [lemma, in rt_opt_util]
Sub_Bound_Unary_Minus_Compat [lemma, in rt_opt_util]
Sub_Bound_Minus_Compat [lemma, in rt_opt_util]
Sub_Bound_Plus_Compat [lemma, in rt_opt_util]
sub_bound_f_completeness [lemma, in rt_opt_impl_consistent]
sub_bound_f_soundness [lemma, in rt_opt_impl_consistent]
SU_Selected_Component_X [constructor, in eval_rt]
SU_Selected_Component_xRTE_X [constructor, in eval_rt]
SU_Indexed_Component_X [constructor, in eval_rt]
SU_Indexed_Component_Range_RTE_X [constructor, in eval_rt]
SU_Indexed_Component_eRTE_X [constructor, in eval_rt]
SU_Indexed_Component_xRTE_X [constructor, in eval_rt]
SU_Identifier_X [constructor, in eval_rt]
SU_Selected_Component [constructor, in eval]
SU_Selected_Component_xRTE [constructor, in eval]
SU_Indexed_Component [constructor, in eval]
SU_Indexed_Component_Range_RTE [constructor, in eval]
SU_Indexed_Component_eRTE [constructor, in eval]
SU_Indexed_Component_xRTE [constructor, in eval]
SU_Identifier [constructor, in eval]
symboltable [library]
SymbolTableM [module, in symboltable_module]
SymbolTableM.Entry_Sloc.T [definition, in symboltable_module]
SymbolTableM.Entry_Sloc [module, in symboltable_module]
SymbolTableM.Entry_Exp_Type.T [definition, in symboltable_module]
SymbolTableM.Entry_Exp_Type [module, in symboltable_module]
SymbolTableM.Entry_Type_Decl.T [definition, in symboltable_module]
SymbolTableM.Entry_Type_Decl [module, in symboltable_module]
SymbolTableM.Entry_Procedure_Decl.T [definition, in symboltable_module]
SymbolTableM.Entry_Procedure_Decl [module, in symboltable_module]
SymbolTableM.Entry_Type.T [definition, in symboltable_module]
SymbolTableM.Entry_Type [module, in symboltable_module]
SymbolTableM.Entry_Name.T [definition, in symboltable_module]
SymbolTableM.Entry_Name [module, in symboltable_module]
SymbolTableM.exps [projection, in symboltable_module]
SymbolTableM.level [definition, in symboltable_module]
SymbolTableM.mkSymbolTable [constructor, in symboltable_module]
SymbolTableM.Names [module, in symboltable_module]
SymbolTableM.names [projection, in symboltable_module]
SymbolTableM.procs [projection, in symboltable_module]
SymbolTableM.proc_decl [definition, in symboltable_module]
SymbolTableM.sloc [projection, in symboltable_module]
SymbolTableM.source_location [definition, in symboltable_module]
SymbolTableM.symboltable [record, in symboltable_module]
SymbolTableM.SymTable_Sloc [module, in symboltable_module]
SymbolTableM.SymTable_Exps [module, in symboltable_module]
SymbolTableM.SymTable_Types [module, in symboltable_module]
SymbolTableM.SymTable_Procs [module, in symboltable_module]
SymbolTableM.SymTable_Vars [module, in symboltable_module]
SymbolTableM.types [projection, in symboltable_module]
SymbolTableM.type_decl [definition, in symboltable_module]
SymbolTableM.vars [projection, in symboltable_module]
symboltable_module [library]
Symbol_Table_Module_RT [module, in symboltable]
Symbol_Table_Module [module, in symboltable]
Symbol_Table_Elements_RT.Source_Location [definition, in symboltable]
Symbol_Table_Elements_RT.Type_Decl [definition, in symboltable]
Symbol_Table_Elements_RT.Procedure_Decl [definition, in symboltable]
Symbol_Table_Elements_RT [module, in symboltable]
Symbol_Table_Elements.Source_Location [definition, in symboltable]
Symbol_Table_Elements.Type_Decl [definition, in symboltable]
Symbol_Table_Elements.Procedure_Decl [definition, in symboltable]
Symbol_Table_Elements [module, in symboltable]
symbol_table_exp_type_eq [lemma, in rt_gen_util]
symbol_table_exp_type_rel [lemma, in rt_gen_util]
symbol_table_type_rel_backward [lemma, in rt_gen_util]
symbol_table_type_rel [lemma, in rt_gen_util]
symbol_table_var_rel [lemma, in rt_gen_util]
symbol_table_procedure_rel_backward [lemma, in rt_gen_util]
symbol_table_procedure_rel [lemma, in rt_gen_util]
symTab [definition, in symboltable]
SymTable_Element.Source_Location [axiom, in symboltable_module]
SymTable_Element.Type_Decl [axiom, in symboltable_module]
SymTable_Element.Procedure_Decl [axiom, in symboltable_module]
SymTable_Element [module, in symboltable_module]
symTabRT [definition, in symboltable]
T
ToArgsIn [constructor, in rt_gen]ToArgsInOut [constructor, in rt_gen]
ToArgsInOutRangeCheck [constructor, in rt_gen]
ToArgsInOutRangeCheckIn [constructor, in rt_gen]
ToArgsInOutRangeCheckOut [constructor, in rt_gen]
ToArgsInRangeCheck [constructor, in rt_gen]
ToArgsNull [constructor, in rt_gen]
ToArgsOut [constructor, in rt_gen]
ToArgsOutRangeCheck [constructor, in rt_gen]
toArgsRT [inductive, in rt_gen]
toArgsRTImpl_completeness [lemma, in rt_gen_impl_consistent]
toArgsRTImpl_soundness [lemma, in rt_gen_impl_consistent]
toArrayTypeDecl [constructor, in rt_gen]
ToAssign [constructor, in rt_gen]
ToAssignRangeCheck [constructor, in rt_gen]
toAssignStmtRT_completeness [lemma, in rt_gen_consistent]
toAssignStmtRT_soundness [lemma, in rt_gen_consistent]
ToBinOpDO [constructor, in rt_gen]
ToBinOpM [constructor, in rt_gen]
ToBinOpO [constructor, in rt_gen]
ToBinOpOthers [constructor, in rt_gen]
ToCall [constructor, in rt_gen]
toDeclRT [inductive, in rt_gen]
toDeclRTConsistent [lemma, in rt_gen_consistent]
toDeclRTImpl_completeness [lemma, in rt_gen_impl_consistent]
toDeclRTImpl_soundness [lemma, in rt_gen_impl_consistent]
toDeclRT_completeness [lemma, in rt_gen_consistent]
toDeclRT_soundness [lemma, in rt_gen_consistent]
toDerivedTypeDecl [constructor, in rt_gen]
toExpRT [inductive, in rt_gen]
toExpRTConsistent [lemma, in rt_gen_consistent]
toExpRTImplConsistent [lemma, in rt_gen_impl_consistent]
toExpRTImpl_completeness [lemma, in rt_gen_impl_consistent]
toExpRTImpl_soundness [lemma, in rt_gen_impl_consistent]
toExpRT_completeness [lemma, in rt_gen_consistent]
toExpRT_soundness [lemma, in rt_gen_consistent]
toIdentifier [constructor, in rt_gen]
ToIf [constructor, in rt_gen]
toIndexedComponent [constructor, in rt_gen]
toIntegerTypeDecl [constructor, in rt_gen]
ToLitBool [constructor, in rt_gen]
ToLitIntF [constructor, in rt_gen]
ToLitIntT [constructor, in rt_gen]
ToName [constructor, in rt_gen]
toNameRT [inductive, in rt_gen]
toNameRTConsistent [lemma, in rt_gen_consistent]
toNameRTImpl_completeness [lemma, in rt_gen_impl_consistent]
toNameRTImpl_soundness [lemma, in rt_gen_impl_consistent]
toNameRT_completeness [lemma, in rt_gen_consistent]
toNameRT_soundness [lemma, in rt_gen_consistent]
ToNull [constructor, in rt_gen]
ToNullDecl [constructor, in rt_gen]
ToObjDecl [constructor, in rt_gen]
ToObjDeclNoneInit [constructor, in rt_gen]
ToObjDeclRangeCheck [constructor, in rt_gen]
toObjDeclRT [inductive, in rt_gen]
toObjDeclRTImpl_completeness [lemma, in rt_gen_impl_consistent]
toObjDeclRTImpl_soundness [lemma, in rt_gen_impl_consistent]
ToObjDecls [constructor, in rt_gen]
ToObjDeclsNull [constructor, in rt_gen]
toObjDeclsRT [inductive, in rt_gen]
toObjDeclsRTImpl_completeness [lemma, in rt_gen_impl_consistent]
toObjDeclsRTImpl_soundness [lemma, in rt_gen_impl_consistent]
ToObjectDecl [constructor, in rt_gen]
ToParamSpec [constructor, in rt_gen]
toParamSpecRT [inductive, in rt_gen]
toParamSpecRTImpl_completeness [lemma, in rt_gen_impl_consistent]
toParamSpecRTImpl_soundness [lemma, in rt_gen_impl_consistent]
ToParamSpecs [constructor, in rt_gen]
ToParamSpecsNull [constructor, in rt_gen]
toParamSpecsRT [inductive, in rt_gen]
toParamSpecsRTImpl_completeness [lemma, in rt_gen_impl_consistent]
toParamSpecsRTImpl_soundness [lemma, in rt_gen_impl_consistent]
ToProcBodyDecl [constructor, in rt_gen]
toProcBodyDeclRT [inductive, in rt_gen]
toProcBodyDeclRTConsistent [lemma, in rt_gen_impl_consistent]
toProcBodyDeclRTImpl_completeness [lemma, in rt_gen_impl_consistent]
toProcBodyDeclRTImpl_soundness [lemma, in rt_gen_impl_consistent]
ToProcDecl [constructor, in rt_gen]
ToProcDeclMap [constructor, in rt_gen_util]
ToProcDeclMapNull [constructor, in rt_gen_util]
toProcDeclRTMap [inductive, in rt_gen_util]
ToProgramRT [constructor, in rt_gen]
toProgramRT [inductive, in rt_gen]
toProgramRTConsistent [lemma, in rt_gen_consistent]
toProgramRTImplConsistent [lemma, in rt_gen_impl_consistent]
toProgramRTImpl_completeness [lemma, in rt_gen_impl_consistent]
toProgramRTImpl_soundness [lemma, in rt_gen_impl_consistent]
toProgramRT_completeness [lemma, in rt_gen_consistent]
toProgramRT_soundness [lemma, in rt_gen_consistent]
toRecordTypeDecl [constructor, in rt_gen]
toSelectedComponent [constructor, in rt_gen]
ToSeq [constructor, in rt_gen]
ToSeqDecl [constructor, in rt_gen]
toStmtRT [inductive, in rt_gen]
toStmtRTConsistent [lemma, in rt_gen_consistent]
toStmtRTImplConsistent [lemma, in rt_gen_impl_consistent]
toStmtRTImpl_completeness [lemma, in rt_gen_impl_consistent]
toStmtRTImpl_soundness [lemma, in rt_gen_impl_consistent]
toStmtRT_completeness [lemma, in rt_gen_consistent]
toStmtRT_soundness [lemma, in rt_gen_consistent]
toSubtypeDecl [constructor, in rt_gen]
ToSymTab [constructor, in rt_gen_util]
toSymTabRT [inductive, in rt_gen_util]
ToTypeDecl [constructor, in rt_gen]
ToTypeDeclMap [constructor, in rt_gen_util]
ToTypeDeclMapNull [constructor, in rt_gen_util]
toTypeDeclRT [inductive, in rt_gen]
toTypeDeclRTImpl_completeness [lemma, in rt_gen_impl_consistent]
toTypeDeclRTImpl_soundness [lemma, in rt_gen_impl_consistent]
toTypeDeclRTMap [inductive, in rt_gen_util]
ToUnOpO [constructor, in rt_gen]
ToUnOpOthers [constructor, in rt_gen]
ToWhile [constructor, in rt_gen]
TProcDecl [constructor, in well_typed]
TStack [constructor, in well_typed]
TStack_SymbolTable [constructor, in well_typed]
TStore [constructor, in well_typed]
TSubtypeDecl [constructor, in well_typed]
TSymbolTable [constructor, in well_typed]
TVStack [constructor, in well_typed]
TVStack_Nil [constructor, in well_typed]
TVStore [constructor, in well_typed]
TVStore_Nil [constructor, in well_typed]
TV_Record_Type [constructor, in well_typed]
TV_Array_Type [constructor, in well_typed]
TV_Integer_Type [constructor, in well_typed]
TV_Derived_Type [constructor, in well_typed]
TV_Subtype [constructor, in well_typed]
TV_Int [constructor, in well_typed]
TV_Bool [constructor, in well_typed]
TV_Undefined [constructor, in well_typed]
type [inductive, in ast_basics]
TypeDecl [constructor, in ast]
typeDecl [inductive, in ast]
TypeDeclRT [constructor, in ast_rt]
typeDeclRT [inductive, in ast_rt]
typed_value_in_bound2 [lemma, in well_typed_util]
typed_value_in_bound1 [lemma, in well_typed_util]
typeNames [projection, in symboltable_module]
typenum [definition, in ast_basics]
type_name [definition, in ast]
type_match_ref [lemma, in well_typed]
type_match [definition, in well_typed]
type_of_exp_x [definition, in well_typed]
type_of_name_x [definition, in well_typed]
type_name_rt [definition, in ast_rt]
type_decl_rt [definition, in symboltable]
type_decl [definition, in symboltable]
type_declaration_rel_backward [lemma, in rt_gen_util]
type_declaration_rel [lemma, in rt_gen_util]
U
Unary_Minus [constructor, in ast_basics]unary_operator [inductive, in ast_basics]
Undefined [constructor, in values]
UndefinedCheck [constructor, in rt]
UnOp [constructor, in ast]
UnOpRT [constructor, in ast_rt]
unop_no_check_flagged_soundness [lemma, in rt_gen_consistent]
unop_no_check_soundness [lemma, in rt_gen_consistent]
unop_flagged_overflow_check_soundness [lemma, in rt_gen_consistent]
unop_overflow_check_soundness [lemma, in rt_gen_consistent]
unop_type [definition, in well_typed]
unop_arithm_operand_format [lemma, in eval_rt]
unop_minus_typed [lemma, in well_typed_util]
unop_arithm_in_bound [lemma, in rt_opt_util]
updated_record_select [lemma, in well_typed_util]
updated_array_select [lemma, in well_typed_util]
updated_record_select_eq [lemma, in well_typed_util]
updated_array_select_eq [lemma, in well_typed_util]
updateG_with_typed_value_preserve_typed_stack [lemma, in well_typed_util]
update_exterior_checks_name_astnum_eq [lemma, in ast_util]
update_exterior_checks_exp_astnum_eq [lemma, in ast_util]
update_exterior_checks_exp [definition, in ast_util]
update_exterior_checks_name [definition, in ast_util]
update_sloc_rt [definition, in symboltable]
update_exps_rt [definition, in symboltable]
update_types_rt [definition, in symboltable]
update_procs_rt [definition, in symboltable]
update_vars_rt [definition, in symboltable]
update_sloc [definition, in symboltable]
update_exps [definition, in symboltable]
update_types [definition, in symboltable]
update_procs [definition, in symboltable]
update_vars [definition, in symboltable]
V
value [inductive, in values]values [library]
value_well_typed_with_matched_type [lemma, in well_typed_util]
value_in_range_is_well_typed [lemma, in well_typed_util]
varNames [projection, in symboltable_module]
W
wellTypedStatePreservation [lemma, in well_typed_util]well_typed_stack_and_symboltable [inductive, in well_typed]
well_typed_stack_infer [lemma, in well_typed]
well_typed_value_in_stack [inductive, in well_typed]
well_typed_stack [inductive, in well_typed]
well_typed_store_infer [lemma, in well_typed]
well_typed_value_in_store [inductive, in well_typed]
well_typed_store [inductive, in well_typed]
well_typed_value [inductive, in well_typed]
well_typed_symbol_table [inductive, in well_typed]
well_typed_proc_declaration [inductive, in well_typed]
well_typed_subtype_declaration [inductive, in well_typed]
well_typed_program_x [inductive, in well_typed]
well_typed_proc_body_x [inductive, in well_typed]
well_typed_decl_x [inductive, in well_typed]
well_typed_type_decl_x [inductive, in well_typed]
well_typed_statement_x [inductive, in well_typed]
well_typed_args_x [inductive, in well_typed]
well_typed_params_x [inductive, in well_typed]
well_typed_exps_x [inductive, in well_typed]
well_typed_name_x [inductive, in well_typed]
well_typed_exp_x [inductive, in well_typed]
well_typed_value_in_store_fetch [lemma, in well_typed_util]
well_typed_int_value_exists [lemma, in well_typed_util]
well_typed_value_subtype_trans [lemma, in well_typed_util]
well_typed_value_of_var [lemma, in well_typed_util]
well_typed_var_in_bound [lemma, in well_typed_util]
well_typed_bounded_var_exists_int_value [lemma, in well_typed_util]
well_typed_stack_split' [lemma, in well_typed_util]
well_typed_store_split' [lemma, in well_typed_util]
well_typed_store_stack_split' [lemma, in well_typed_util]
well_typed_stacks_merge' [lemma, in well_typed_util]
well_typed_store_merge' [lemma, in well_typed_util]
well_typed_store_stack_merge' [lemma, in well_typed_util]
well_typed_store_updated_by_undefined_value' [lemma, in well_typed_util]
well_typed_stacks_merge [lemma, in well_typed_util]
well_typed_store_stack_merge [lemma, in well_typed_util]
well_typed_store_updated_by_undefined_value [lemma, in well_typed_util]
well_typed_name_preserve [lemma, in well_typed_util]
well_typed_exp_preserve [lemma, in well_typed_util]
well_typed_util [library]
well_typed [library]
While [constructor, in ast]
WhileRT [constructor, in ast_rt]
wordsize [definition, in values]
WT_Program_X [constructor, in well_typed]
WT_Proc_Body_X [constructor, in well_typed]
WT_Seq_Decl_X [constructor, in well_typed]
WT_Procedure_Body_X [constructor, in well_typed]
WT_Object_Decl_X [constructor, in well_typed]
WT_Object_Decl_None_Init_X [constructor, in well_typed]
WT_Type_Decl_X [constructor, in well_typed]
WT_Null_Decl_X [constructor, in well_typed]
WT_Record_Type_Decl_X [constructor, in well_typed]
WT_Array_Type_Decl_X [constructor, in well_typed]
WT_Int_Type_Decl_X [constructor, in well_typed]
WT_Derived_Type_Decl_X [constructor, in well_typed]
WT_Subtype_Decl_X [constructor, in well_typed]
WT_Sequence_X [constructor, in well_typed]
WT_Procedure_Call_X [constructor, in well_typed]
WT_While_X [constructor, in well_typed]
WT_If_X [constructor, in well_typed]
WT_Assignment_X [constructor, in well_typed]
WT_Null_X [constructor, in well_typed]
WT_Args_X [constructor, in well_typed]
WT_Args_Nil_X [constructor, in well_typed]
WT_Params_X [constructor, in well_typed]
WT_Params_Nil_X [constructor, in well_typed]
WT_Exps_X [constructor, in well_typed]
WT_Exps_Nil_X [constructor, in well_typed]
WT_Selected_Component_X [constructor, in well_typed]
WT_Indexed_Component_X [constructor, in well_typed]
WT_Identifier_X [constructor, in well_typed]
WT_Unary_Exp_X [constructor, in well_typed]
WT_Binary_Exp_X [constructor, in well_typed]
WT_Name_X [constructor, in well_typed]
WT_Literal_Bool_X [constructor, in well_typed]
WT_Literal_Int_X [constructor, in well_typed]
Z
Zabs_quot_neg1 [lemma, in rt_opt_ZArith]Zabs_ge_neg_v [lemma, in rt_opt_ZArith]
Zabs_ge_v [lemma, in rt_opt_ZArith]
Zeqb_eq [lemma, in rt_opt_ZArith]
Zgele_Bool_Imp_GeLe_F [lemma, in rt_opt_ZArith]
Zgele_Bool_Imp_GeLe_T [lemma, in rt_opt_ZArith]
Zge_p1_0 [lemma, in rt_opt_ZArith]
Zge_le_bool [lemma, in rt_opt_ZArith]
Zgt_lt_bool [lemma, in rt_opt_ZArith]
Zleb_trans [lemma, in rt_opt_ZArith]
Zleb_ltb_trans_ltb [lemma, in rt_opt_ZArith]
Zleb_ltb_trans_leb [lemma, in rt_opt_ZArith]
Zleb_true_le_true [lemma, in rt_opt_ZArith]
Zleb_le [lemma, in rt_opt_ZArith]
Zlele_Bool_Imp_LeLe_F [lemma, in rt_opt_ZArith]
Zlele_Bool_Imp_LeLe_T [lemma, in rt_opt_ZArith]
Zle_n1_0 [lemma, in rt_opt_ZArith]
Zle_eq_e_r [lemma, in rt_opt_ZArith]
Zle_eq_e_l [lemma, in rt_opt_ZArith]
Zle_ge_bool [lemma, in rt_opt_ZArith]
Zle_true_leb_true [lemma, in rt_opt_ZArith]
Zltb_succ_l [lemma, in rt_opt_ZArith]
Zltb_pred_r [lemma, in rt_opt_ZArith]
Zltb_trans [lemma, in rt_opt_ZArith]
Zltb_leb_trans_ltb [lemma, in rt_opt_ZArith]
Zltb_leb_trans_leb [lemma, in rt_opt_ZArith]
Zltb_imp_leb [lemma, in rt_opt_ZArith]
Zltb_lt [lemma, in rt_opt_ZArith]
Zlt_le_pred_r [lemma, in rt_opt_ZArith]
Zlt_le_succ_l [lemma, in rt_opt_ZArith]
Zlt_le [lemma, in rt_opt_ZArith]
Zlt_gt_bool [lemma, in rt_opt_ZArith]
Zmult_le_rev_r [lemma, in rt_opt_ZArith]
Zmult_le_rev_l [lemma, in rt_opt_ZArith]
Zmult_le_ge_l [lemma, in rt_opt_ZArith]
Zmult_le_ge_r [lemma, in rt_opt_ZArith]
Zmult_lt_lt [lemma, in rt_opt_ZArith]
Zmult_le_lt [lemma, in rt_opt_ZArith]
Zmult_le_le [lemma, in rt_opt_ZArith]
Zquot_n1_interval [lemma, in rt_opt_ZArith]
Zquot_p1_interval [lemma, in rt_opt_ZArith]
Zquot_n1_opp [lemma, in rt_opt_ZArith]
Zquot_n_p_n [lemma, in rt_opt_ZArith]
Zquot_p_n_n [lemma, in rt_opt_ZArith]
Zquot_n_n_p [lemma, in rt_opt_ZArith]
Zquot_p_p_p [lemma, in rt_opt_ZArith]
Zquot_le_compat_n_n [lemma, in rt_opt_ZArith]
Zquot_le_compat_p_n [lemma, in rt_opt_ZArith]
Zquot_le_compat_n_p [lemma, in rt_opt_ZArith]
Zquot_le_compat_p_p [lemma, in rt_opt_ZArith]
Zquot_antitone [lemma, in rt_opt_ZArith]
Module Index
E
ENTRY [in environment]Entry_Value_Stored [in eval]
M
Math [in values]S
STACK [in eval]STORE [in environment]
SymbolTableM [in symboltable_module]
SymbolTableM.Entry_Sloc [in symboltable_module]
SymbolTableM.Entry_Exp_Type [in symboltable_module]
SymbolTableM.Entry_Type_Decl [in symboltable_module]
SymbolTableM.Entry_Procedure_Decl [in symboltable_module]
SymbolTableM.Entry_Type [in symboltable_module]
SymbolTableM.Entry_Name [in symboltable_module]
SymbolTableM.Names [in symboltable_module]
SymbolTableM.SymTable_Sloc [in symboltable_module]
SymbolTableM.SymTable_Exps [in symboltable_module]
SymbolTableM.SymTable_Types [in symboltable_module]
SymbolTableM.SymTable_Procs [in symboltable_module]
SymbolTableM.SymTable_Vars [in symboltable_module]
Symbol_Table_Module_RT [in symboltable]
Symbol_Table_Module [in symboltable]
Symbol_Table_Elements_RT [in symboltable]
Symbol_Table_Elements [in symboltable]
SymTable_Element [in symboltable_module]
Library Index
A
astast_util
ast_rt
ast_basics
C
CpdtTacticsE
environmenteval
eval_rt
L
list_utilR
rtrt_gen_util
rt_validator
rt_opt
rt_gen
rt_counter
rt_opt_consistent
rt_opt_consistent_util
rt_opt_impl
rt_opt_util
rt_gen_consistent
rt_opt_ZArith
rt_gen_impl
rt_opt_impl_consistent
rt_gen_impl_consistent
S
symboltablesymboltable_module
V
valuesW
well_typed_utilwell_typed
Constructor Index
A
Aggregate [in values]And [in ast_basics]
ArrayTypeDecl [in ast]
ArrayTypeDeclRT [in ast_rt]
ArrayV [in values]
Array_Type [in ast_basics]
Assign [in ast]
AssignRT [in ast_rt]
B
BinOp [in ast]BinOpRT [in ast_rt]
Bool [in values]
Boolean [in ast_basics]
Boolean_Literal [in ast_basics]
Boolval [in values]
C
Call [in ast]CallRT [in ast_rt]
CheckBinOpNil [in eval_rt]
ChecksBinOp [in eval_rt]
ChecksBinOpRTE [in eval_rt]
cks_infor [in rt_counter]
CopyIn_Mode_Out_X [in eval_rt]
CopyIn_Mode_InOut_Range_X [in eval_rt]
CopyIn_Mode_InOut_Range_RTE_X [in eval_rt]
CopyIn_Mode_InOut_NoRange_X [in eval_rt]
CopyIn_Mode_InOut_eRTE_X [in eval_rt]
CopyIn_Mode_In_Range_X [in eval_rt]
CopyIn_Mode_In_Range_RTE_X [in eval_rt]
CopyIn_Mode_In_NoRangeCheck_X [in eval_rt]
CopyIn_Mode_In_eRTE_X [in eval_rt]
CopyIn_Nil_X [in eval_rt]
CopyIn_Mode_Out [in eval]
CopyIn_Mode_InOut_Range [in eval]
CopyIn_Mode_InOut_Range_RTE [in eval]
CopyIn_Mode_InOut_NoRange [in eval]
CopyIn_Mode_InOut_eRTE [in eval]
CopyIn_Mode_In_Range [in eval]
CopyIn_Mode_In_Range_RTE [in eval]
CopyIn_Mode_In_NoRange [in eval]
CopyIn_Mode_In_eRTE [in eval]
CopyIn_Nil [in eval]
CopyOut_Mode_In_X [in eval_rt]
CopyOut_Mode_Out_Range_X [in eval_rt]
CopyOut_Mode_Out_Range_nRTE_X [in eval_rt]
CopyOut_Mode_Out_Range_RTE_X [in eval_rt]
CopyOut_Mode_Out_NoRange_X [in eval_rt]
CopyOut_Mode_Out_nRTE_X [in eval_rt]
CopyOut_Nil_X [in eval_rt]
CopyOut_Mode_In [in eval]
CopyOut_Mode_Out_Range [in eval]
CopyOut_Mode_Out_Range_nRTE [in eval]
CopyOut_Mode_Out_Range_RTE [in eval]
CopyOut_Mode_Out_NoRange [in eval]
CopyOut_Mode_Out_nRTE [in eval]
CopyOut_Nil [in eval]
CutUntil_Tail [in eval]
CutUntil_Head [in eval]
CutUntil_Nil [in eval]
D
DerivedTypeDecl [in ast]DerivedTypeDeclRT [in ast_rt]
Derived_Type [in ast_basics]
diff [in rt_validator]
diff' [in rt_validator]
DivByZero [in values]
DivCheck [in rt]
DivCheckBinop [in eval_rt]
DivCheck_M [in eval]
DivCheck_D [in eval]
DivCheck_RTE [in eval]
Divide [in ast_basics]
DoCheckOnBinops [in eval]
DoCheckOnBinOp_Others [in eval]
DoCheckOnDivide [in eval]
DoCheckOnDivide_RTE [in eval]
DoCheckOnModulus [in eval]
DoCheckOnUnary_Minus [in eval]
DoCheckOnUnOp_Others [in eval]
Do_Checks_Unop [in eval_rt]
Do_Checks_Unop_RTE [in eval_rt]
Do_Check_Unop_Nil [in eval_rt]
E
Equal [in ast_basics]Error [in rt_validator]
Error' [in rt_validator]
EvalAssign [in eval]
EvalAssignRT [in eval_rt]
EvalAssignRT_Range [in eval_rt]
EvalAssignRT_Range_RTE [in eval_rt]
EvalAssignRT_RTE [in eval_rt]
EvalAssign_Range [in eval]
EvalAssign_Range_RTE [in eval]
EvalAssign_RTE [in eval]
EvalBinOp [in eval]
EvalBinOpE1_RTE [in eval]
EvalBinOpE2_RTE [in eval]
EvalBinOpRT [in eval_rt]
EvalBinOpRTE1_RTE [in eval_rt]
EvalBinOpRTE2_RTE [in eval_rt]
EvalCall [in eval]
EvalCallRT [in eval_rt]
EvalCallRT_Body_RTE [in eval_rt]
EvalCallRT_Decl_RTE [in eval_rt]
EvalCallRT_Args_RTE [in eval_rt]
EvalCall_Body_RTE [in eval]
EvalCall_Decl_RTE [in eval]
EvalCall_Args_RTE [in eval]
EvalDeclRT_Seq [in eval_rt]
EvalDeclRT_Seq_E [in eval_rt]
EvalDeclRT_Proc [in eval_rt]
EvalDeclRT_Type [in eval_rt]
EvalDeclRT_Var [in eval_rt]
EvalDeclRT_Var_Range_RTE [in eval_rt]
EvalDeclRT_Var_NoCheck [in eval_rt]
EvalDeclRT_Var_RTE [in eval_rt]
EvalDeclRT_Var_None [in eval_rt]
EvalDeclRT_Null [in eval_rt]
EvalDecl_Seq [in eval]
EvalDecl_Seq_RTE [in eval]
EvalDecl_Proc [in eval]
EvalDecl_Var_Range [in eval]
EvalDecl_Var_Range_RTE [in eval]
EvalDecl_Var [in eval]
EvalDecl_Var_RTE [in eval]
EvalDecl_Var_None [in eval]
EvalDecl_Type [in eval]
EvalDecl_Null [in eval]
EvalIdentifier [in eval]
EvalIdentifierRT [in eval_rt]
EvalIfRT_False [in eval_rt]
EvalIfRT_True [in eval_rt]
EvalIfRT_RTE [in eval_rt]
EvalIf_False [in eval]
EvalIf_True [in eval]
EvalIf_RTE [in eval]
EvalIndexedComponent [in eval]
EvalIndexedComponentE_RTE [in eval]
EvalIndexedComponentRT [in eval_rt]
EvalIndexedComponentRTE_RTE [in eval_rt]
EvalIndexedComponentRTX_RTE [in eval_rt]
EvalIndexedComponentRT_Range_RTE [in eval_rt]
EvalIndexedComponentX_RTE [in eval]
EvalIndexedComponent_Range_RTE [in eval]
EvalLiteral [in eval]
EvalLiteralRT [in eval_rt]
EvalLiteralRT_Int [in eval_rt]
EvalLiteralRT_Bool [in eval_rt]
EvalLiteral_Int [in eval]
EvalLiteral_Bool [in eval]
EvalName [in eval]
EvalNameRT [in eval_rt]
EvalNull [in eval]
EvalNullRT [in eval_rt]
EvalProgram [in eval]
EvalProgramRT [in eval_rt]
EvalSelectedComponent [in eval]
EvalSelectedComponentRT [in eval_rt]
EvalSelectedComponentRTX_RTE [in eval_rt]
EvalSelectedComponentX_RTE [in eval]
EvalSeq [in eval]
EvalSeqRT [in eval_rt]
EvalSeqRT_RTE [in eval_rt]
EvalSeq_RTE [in eval]
EvalUnOp [in eval]
EvalUnOpRT [in eval_rt]
EvalUnOpRT_RTE [in eval_rt]
EvalUnOp_RTE [in eval]
EvalWhileRT_False [in eval_rt]
EvalWhileRT_True [in eval_rt]
EvalWhileRT_True_RTE [in eval_rt]
EvalWhileRT_RTE [in eval_rt]
EvalWhile_False [in eval]
EvalWhile_True [in eval]
EvalWhile_True_RTE [in eval]
EvalWhile_RTE [in eval]
Extract_Index_Range_RT [in symboltable]
Extract_Range_RT [in symboltable]
Extract_Index_Range [in symboltable]
Extract_Range [in symboltable]
G
Greater_Than_Or_Equal [in ast_basics]Greater_Than [in ast_basics]
I
IB_False [in values]IB_True [in values]
Identifier [in ast]
IdentifierRT [in ast_rt]
If [in ast]
IfRT [in ast_rt]
In [in ast_basics]
IndexedComponent [in ast]
IndexedComponentRT [in ast_rt]
Int [in values]
Integer [in ast_basics]
IntegerTypeDecl [in ast]
IntegerTypeDeclRT [in ast_rt]
Integer_Literal [in ast_basics]
Integer_Type [in ast_basics]
Interval [in values]
In_Out [in ast_basics]
L
Less_Than_Or_Equal [in ast_basics]Less_Than [in ast_basics]
Literal [in ast]
LiteralRT [in ast_rt]
M
Minus [in ast_basics]Mismatch [in rt_validator]
Mismatch' [in rt_validator]
mkNameTable [in symboltable_module]
mkobjDecl [in ast]
mkobjDeclRT [in ast_rt]
mkparamSpec [in ast]
mkparamSpecRT [in ast_rt]
mkprocBodyDecl [in ast]
mkprocBodyDeclRT [in ast_rt]
mkprogram [in ast]
mkprogramRT [in ast_rt]
Modulus [in ast_basics]
Multiply [in ast_basics]
N
Name [in ast]NameRT [in ast_rt]
Not [in ast_basics]
Not_Equal [in ast_basics]
not_inbetween_opt_cmp_cks [in rt_validator]
not_subset_of_cmp_cks [in rt_validator]
not_superset_of_opt_cks [in rt_validator]
Null [in ast]
NullDecl [in ast]
NullDeclRT [in ast_rt]
NullRT [in ast_rt]
O
ObjDecl [in ast]ObjDeclRT [in ast_rt]
OK [in values]
OK [in rt_validator]
OK' [in rt_validator]
Or [in ast_basics]
Out [in ast_basics]
OverflowCheck [in rt]
OverflowCheckBinop [in eval_rt]
OverflowCheckUnop [in eval_rt]
OverflowCheck_List [in eval_rt]
OverflowCheck_Nil [in eval_rt]
OverflowCheck_OK [in eval]
OverflowCheck_Fail [in eval]
OverflowError [in values]
P
Plus [in ast_basics]ProcBodyDecl [in ast]
ProcBodyDeclRT [in ast_rt]
R
Range [in ast]RangeCheck [in rt]
RangeCheckOnReturn [in rt]
RangeCheck_List [in eval_rt]
RangeCheck_Nil [in eval_rt]
RangeCheck_OK [in eval]
RangeCheck_Fail [in eval]
RangeError [in values]
RangeRT [in ast_rt]
RecordTypeDecl [in ast]
RecordTypeDeclRT [in ast_rt]
RecordV [in values]
Record_Type [in ast_basics]
RTE [in values]
S
SelectedComponent [in ast]SelectedComponentRT [in ast_rt]
Seq [in ast]
SeqDecl [in ast]
SeqDeclRT [in ast_rt]
SeqRT [in ast_rt]
sloc [in symboltable]
STORE.eqncons [in environment]
STORE.eqnil [in environment]
Subtype [in ast_basics]
SubtypeDecl [in ast]
SubtypeDeclRT [in ast_rt]
SU_Selected_Component_X [in eval_rt]
SU_Selected_Component_xRTE_X [in eval_rt]
SU_Indexed_Component_X [in eval_rt]
SU_Indexed_Component_Range_RTE_X [in eval_rt]
SU_Indexed_Component_eRTE_X [in eval_rt]
SU_Indexed_Component_xRTE_X [in eval_rt]
SU_Identifier_X [in eval_rt]
SU_Selected_Component [in eval]
SU_Selected_Component_xRTE [in eval]
SU_Indexed_Component [in eval]
SU_Indexed_Component_Range_RTE [in eval]
SU_Indexed_Component_eRTE [in eval]
SU_Indexed_Component_xRTE [in eval]
SU_Identifier [in eval]
SymbolTableM.mkSymbolTable [in symboltable_module]
T
ToArgsIn [in rt_gen]ToArgsInOut [in rt_gen]
ToArgsInOutRangeCheck [in rt_gen]
ToArgsInOutRangeCheckIn [in rt_gen]
ToArgsInOutRangeCheckOut [in rt_gen]
ToArgsInRangeCheck [in rt_gen]
ToArgsNull [in rt_gen]
ToArgsOut [in rt_gen]
ToArgsOutRangeCheck [in rt_gen]
toArrayTypeDecl [in rt_gen]
ToAssign [in rt_gen]
ToAssignRangeCheck [in rt_gen]
ToBinOpDO [in rt_gen]
ToBinOpM [in rt_gen]
ToBinOpO [in rt_gen]
ToBinOpOthers [in rt_gen]
ToCall [in rt_gen]
toDerivedTypeDecl [in rt_gen]
toIdentifier [in rt_gen]
ToIf [in rt_gen]
toIndexedComponent [in rt_gen]
toIntegerTypeDecl [in rt_gen]
ToLitBool [in rt_gen]
ToLitIntF [in rt_gen]
ToLitIntT [in rt_gen]
ToName [in rt_gen]
ToNull [in rt_gen]
ToNullDecl [in rt_gen]
ToObjDecl [in rt_gen]
ToObjDeclNoneInit [in rt_gen]
ToObjDeclRangeCheck [in rt_gen]
ToObjDecls [in rt_gen]
ToObjDeclsNull [in rt_gen]
ToObjectDecl [in rt_gen]
ToParamSpec [in rt_gen]
ToParamSpecs [in rt_gen]
ToParamSpecsNull [in rt_gen]
ToProcBodyDecl [in rt_gen]
ToProcDecl [in rt_gen]
ToProcDeclMap [in rt_gen_util]
ToProcDeclMapNull [in rt_gen_util]
ToProgramRT [in rt_gen]
toRecordTypeDecl [in rt_gen]
toSelectedComponent [in rt_gen]
ToSeq [in rt_gen]
ToSeqDecl [in rt_gen]
toSubtypeDecl [in rt_gen]
ToSymTab [in rt_gen_util]
ToTypeDecl [in rt_gen]
ToTypeDeclMap [in rt_gen_util]
ToTypeDeclMapNull [in rt_gen_util]
ToUnOpO [in rt_gen]
ToUnOpOthers [in rt_gen]
ToWhile [in rt_gen]
TProcDecl [in well_typed]
TStack [in well_typed]
TStack_SymbolTable [in well_typed]
TStore [in well_typed]
TSubtypeDecl [in well_typed]
TSymbolTable [in well_typed]
TVStack [in well_typed]
TVStack_Nil [in well_typed]
TVStore [in well_typed]
TVStore_Nil [in well_typed]
TV_Record_Type [in well_typed]
TV_Array_Type [in well_typed]
TV_Integer_Type [in well_typed]
TV_Derived_Type [in well_typed]
TV_Subtype [in well_typed]
TV_Int [in well_typed]
TV_Bool [in well_typed]
TV_Undefined [in well_typed]
TypeDecl [in ast]
TypeDeclRT [in ast_rt]
U
Unary_Minus [in ast_basics]Undefined [in values]
UndefinedCheck [in rt]
UnOp [in ast]
UnOpRT [in ast_rt]
W
While [in ast]WhileRT [in ast_rt]
WT_Program_X [in well_typed]
WT_Proc_Body_X [in well_typed]
WT_Seq_Decl_X [in well_typed]
WT_Procedure_Body_X [in well_typed]
WT_Object_Decl_X [in well_typed]
WT_Object_Decl_None_Init_X [in well_typed]
WT_Type_Decl_X [in well_typed]
WT_Null_Decl_X [in well_typed]
WT_Record_Type_Decl_X [in well_typed]
WT_Array_Type_Decl_X [in well_typed]
WT_Int_Type_Decl_X [in well_typed]
WT_Derived_Type_Decl_X [in well_typed]
WT_Subtype_Decl_X [in well_typed]
WT_Sequence_X [in well_typed]
WT_Procedure_Call_X [in well_typed]
WT_While_X [in well_typed]
WT_If_X [in well_typed]
WT_Assignment_X [in well_typed]
WT_Null_X [in well_typed]
WT_Args_X [in well_typed]
WT_Args_Nil_X [in well_typed]
WT_Params_X [in well_typed]
WT_Params_Nil_X [in well_typed]
WT_Exps_X [in well_typed]
WT_Exps_Nil_X [in well_typed]
WT_Selected_Component_X [in well_typed]
WT_Indexed_Component_X [in well_typed]
WT_Identifier_X [in well_typed]
WT_Unary_Exp_X [in well_typed]
WT_Binary_Exp_X [in well_typed]
WT_Name_X [in well_typed]
WT_Literal_Bool_X [in well_typed]
WT_Literal_Int_X [in well_typed]
Lemma Index
A
app_same_length_eq2 [in list_util]app_same_length_eq [in list_util]
arrayUpdate_with_typed_value_preserve_typed_array [in well_typed_util]
B
beq_type_eq [in ast_basics]beq_type_refl [in ast_basics]
binop_no_check_flagged_soundness [in rt_gen_consistent]
binop_no_check_soundness [in rt_gen_consistent]
binop_flagged_division_check_soundness [in rt_gen_consistent]
binop_division_check_soundness [in rt_gen_consistent]
binop_flagged_overflow_division_check_soundness [in rt_gen_consistent]
binop_overflow_division_check_soundness [in rt_gen_consistent]
binop_flagged_overflow_check_soundness [in rt_gen_consistent]
binop_overflow_check_soundness [in rt_gen_consistent]
binop_arithm_operand_format [in eval_rt]
binop_logic_typed [in well_typed_util]
binop_arithm_typed [in well_typed_util]
binop_bool_type [in well_typed_util]
binop_int_type [in well_typed_util]
binop_int_operant_exists [in rt_opt_consistent_util]
bound_of_record_field_type_f_completeness [in rt_opt_impl_consistent]
bound_of_record_field_type_f_soundness [in rt_opt_impl_consistent]
bound_of_array_component_type_f_completeness [in rt_opt_impl_consistent]
bound_of_array_component_type_f_soundness [in rt_opt_impl_consistent]
bound_of_type_f_completeness [in rt_opt_impl_consistent]
bound_of_type_f_soundness [in rt_opt_impl_consistent]
C
check_flag_in_reserve2 [in rt_opt_util]check_flag_in_reserve [in rt_opt_util]
copyInRT_completeness [in rt_gen_consistent]
copyInRT_soundness [in rt_gen_consistent]
copyOutRT_completeness [in rt_gen_consistent]
copyOutRT_soundness [in rt_gen_consistent]
copy_out_preserve_typed_stack [in well_typed_util]
copy_in_preserve_typed_store [in well_typed_util]
cut_until_preserve_typed_stack [in well_typed_util]
cut_until_uniqueness [in eval]
D
divide_result_in_bound_backward [in rt_opt_util]divide_result_in_bound [in rt_opt_util]
divide_in_bound [in rt_opt_ZArith]
do_flagged_checks_on_plus_reserve [in rt_opt_util]
do_flagged_checks_on_modulus_reserve [in rt_opt_util]
do_flagged_checks_on_divide_reserve [in rt_opt_util]
do_range_check_same_result [in rt_opt_util]
do_range_checks_reserve [in rt_opt_util]
do_overflow_checks_reserve [in rt_opt_util]
E
evalUnOpRTS_reserve [in rt_opt_util]eval_name_ex_cks_stripped [in eval_rt]
eval_exp_ex_cks_stripped [in eval_rt]
eval_name_ex_cks_added [in eval_rt]
eval_exp_ex_cks_added [in eval_rt]
eval_statement_preserve_typed_stack [in well_typed_util]
eval_declaration_preserve_typed_store [in well_typed_util]
eval_name_well_typed_value [in well_typed_util]
eval_expr_well_typed_value [in well_typed_util]
eval_expr_value_copy_out_opt_reserve_backward [in rt_opt_util]
eval_expr_value_copy_out_opt_reserve [in rt_opt_util]
eval_expr_value_reserve_backward [in rt_opt_util]
eval_expr_value_reserve [in rt_opt_util]
eval_name_value_in_bound' [in rt_opt_consistent_util]
eval_expr_value_in_bound' [in rt_opt_consistent_util]
eval_name_value_in_bound [in rt_opt_consistent_util]
eval_expr_value_in_bound [in rt_opt_consistent_util]
exp_exterior_checks_refl [in ast_util]
exp_updated_exterior_checks [in ast_util]
exp_type_same [in well_typed_util]
exp_exterior_checks_beq_nil [in rt_gen_util]
exp_ast_num_eq [in rt_gen_util]
extract_subtype_range_unique [in symboltable]
extract_array_index_range_rt_unique [in symboltable]
extract_array_index_range_f_completeness [in rt_opt_impl_consistent]
extract_array_index_range_f_soundness [in rt_opt_impl_consistent]
extract_subtype_range_f_completeness [in rt_opt_impl_consistent]
extract_subtype_range_f_soundness [in rt_opt_impl_consistent]
F
fetchG_split [in well_typed_util]I
index_range_rel_backward [in rt_gen_util]index_range_rel [in rt_gen_util]
in_bound_unique [in rt_opt_util]
in_bound_value_neq_zero [in rt_opt_util]
In_Bound_Unary_Minus_Compat [in rt_opt_util]
In_Bound_Minus_Compat [in rt_opt_util]
In_Bound_Plus_Compat [in rt_opt_util]
In_Bound_Two [in rt_opt_util]
In_Bound_SubBound_Trans [in rt_opt_util]
In_Bound_Trans [in rt_opt_util]
in_bound_conflict [in rt_opt_util]
In_Bound_Refl [in rt_opt_util]
in_bound_f_completeness [in rt_opt_impl_consistent]
in_bound_f_soundness [in rt_opt_impl_consistent]
L
leb_lt_false [in rt_opt_ZArith]length_invcons [in list_util]
length_invnil [in list_util]
le_max_rr [in rt_opt_ZArith]
le_max_rl [in rt_opt_ZArith]
le_max_lr [in rt_opt_ZArith]
le_max_ll [in rt_opt_ZArith]
le_min_rr [in rt_opt_ZArith]
le_min_rl [in rt_opt_ZArith]
le_min_lr [in rt_opt_ZArith]
le_min_ll [in rt_opt_ZArith]
Le_Neg_Ge [in rt_opt_ZArith]
Le_False_Lt [in rt_opt_ZArith]
literal_checks_optimization_soundness [in rt_opt_util]
Lte_Lt_Bool_False [in rt_opt_ZArith]
Lt_Neg_Gt [in rt_opt_ZArith]
Lt_False_Le [in rt_opt_ZArith]
Lt_Le_Bool_False [in rt_opt_ZArith]
M
max_abs_f_ge0 [in rt_opt_ZArith]max_abs_f_opp_le0 [in rt_opt_ZArith]
modulus_result_in_bound_backward [in rt_opt_util]
modulus_result_in_bound [in rt_opt_util]
modulus_in_bound_trans [in rt_opt_util]
modulus_in_int32_bound [in rt_opt_util]
modulus_in_bound [in rt_opt_ZArith]
multiply_in_bound [in rt_opt_ZArith]
N
name_exterior_checks_refl [in ast_util]name_updated_exterior_checks [in ast_util]
name_exterior_checks_beq_nil [in rt_gen_util]
name_ast_num_eq [in rt_gen_util]
O
optArgsImpl_completeness [in rt_opt_impl_consistent]optArgsImpl_soundness [in rt_opt_impl_consistent]
optArgs_copyout_completeness [in rt_opt_consistent]
optArgs_copyout_soundness [in rt_opt_consistent]
optArgs_copyin_soundness' [in rt_opt_consistent_util]
optArgs_copyin_completeness' [in rt_opt_consistent_util]
optArgs_copyin_completeness [in rt_opt_consistent_util]
optArgs_copyin_soundness [in rt_opt_consistent_util]
optDeclConsistent [in rt_opt_consistent]
optDeclImplConsistent [in rt_opt_impl_consistent]
optDeclImpl_completeness [in rt_opt_impl_consistent]
optDeclImpl_soundness [in rt_opt_impl_consistent]
optDecl_completeness [in rt_opt_consistent]
optDecl_soundness [in rt_opt_consistent]
optExpConsistent [in rt_opt_consistent]
optExpImplConsistent [in rt_opt_impl_consistent]
optExpImpl_completeness [in rt_opt_impl_consistent]
optExpImpl_soundness [in rt_opt_impl_consistent]
optExp_soundness' [in rt_opt_consistent_util]
optExp_completeness' [in rt_opt_consistent_util]
optExp_completeness [in rt_opt_consistent_util]
optExp_soundness [in rt_opt_consistent_util]
optimize_name_ex_cks_stripped [in rt_opt_util]
optimize_exp_ex_cks_stripped [in rt_opt_util]
optimize_range_check_on_copy_out_reserve [in rt_opt_util]
optimize_range_check_reserve [in rt_opt_util]
optimize_overflow_check_reserve [in rt_opt_util]
optimize_range_check_backward [in rt_opt_util]
optimize_range_check_preserve_backward [in rt_opt_util]
optimize_range_check_preserve [in rt_opt_util]
optimize_name_ex_cks_eq [in rt_opt_util]
optimize_exp_ex_cks_eq [in rt_opt_util]
optimize_name_ast_num_eq [in rt_opt_util]
optimize_name_exist_int_value [in rt_opt_consistent_util]
optimize_expression_exist_int_value [in rt_opt_consistent_util]
optimize_range_check_both_reserve_storeUpdate_backward [in rt_opt_consistent_util]
optimize_range_check_both_reserve_storeUpdate [in rt_opt_consistent_util]
optimize_range_check_on_copy_out_reserve_storeUpdate_backward [in rt_opt_consistent_util]
optimize_range_check_on_copy_out_reserve_storeUpdate [in rt_opt_consistent_util]
optimize_range_check_reserve_storeUpdate_backward [in rt_opt_consistent_util]
optimize_range_check_reserve_storeUpdate [in rt_opt_consistent_util]
optimize_rtc_unop_f_completeness [in rt_opt_impl_consistent]
optimize_rtc_unop_f_soundness [in rt_opt_impl_consistent]
optimize_rtc_binop_f_completeness [in rt_opt_impl_consistent]
optimize_rtc_binop_f_soundness [in rt_opt_impl_consistent]
optimize_range_check_on_copy_out_f_completeness [in rt_opt_impl_consistent]
optimize_range_check_on_copy_out_f_soundness [in rt_opt_impl_consistent]
optimize_range_check_f_completeness [in rt_opt_impl_consistent]
optimize_range_check_f_soundness [in rt_opt_impl_consistent]
optimize_overflow_check_f_completeness [in rt_opt_impl_consistent]
optimize_overflow_check_f_soundness [in rt_opt_impl_consistent]
optLiteralImpl_completeness [in rt_opt_impl_consistent]
optLiteralImpl_soundness [in rt_opt_impl_consistent]
optNameImplConsistent [in rt_opt_impl_consistent]
optNameImpl_completeness [in rt_opt_impl_consistent]
optNameImpl_soundness [in rt_opt_impl_consistent]
optName_soundness' [in rt_opt_consistent_util]
optName_completeness' [in rt_opt_consistent_util]
optName_completeness [in rt_opt_consistent_util]
optName_soundness [in rt_opt_consistent_util]
optObjDeclImpl_completeness [in rt_opt_impl_consistent]
optObjDeclImpl_soundness [in rt_opt_impl_consistent]
optProgramConsistent [in rt_opt_consistent]
optProgramImplConsistent [in rt_opt_impl_consistent]
optProgramImpl_completeness [in rt_opt_impl_consistent]
optProgramImpl_soundness [in rt_opt_impl_consistent]
optProgram_completeness [in rt_opt_consistent]
optProgram_soundness [in rt_opt_consistent]
optStmtConsistent [in rt_opt_consistent]
optStmtImplConsistent [in rt_opt_impl_consistent]
optStmtImpl_completeness [in rt_opt_impl_consistent]
optStmtImpl_soundness [in rt_opt_impl_consistent]
optStmt_completeness [in rt_opt_consistent]
optStmt_soundness [in rt_opt_consistent]
overflow_check_OK_exist_int [in rt_gen_consistent]
P
plus_result_in_bound_backward [in rt_opt_util]plus_result_in_bound [in rt_opt_util]
procedure_declaration_rel_backward [in rt_gen_util]
procedure_declaration_rel [in rt_gen_util]
procedure_components_rel [in rt_gen_util]
push_typed_value_preserve_typed_store [in well_typed_util]
push_value_in_range_preserve_typed_store [in well_typed_util]
R
range_constrainted_type_true [in well_typed_util]range_check_opt_subBound_true [in rt_opt_util]
range_check_on_copyout_preserve [in rt_opt_util]
range_constrainted_type_true [in rt_opt_impl_consistent]
recordUpdate_with_typed_value_preserve_typed_array [in well_typed_util]
removed_check_flag_notin [in rt_opt_util]
remove_check_on_unop_reserve [in rt_opt_util]
remove_check_on_binop_reserve [in rt_opt_util]
remove_notin_check_flag [in rt_opt_util]
S
safe_remove_unop_check [in rt_opt_util]safe_remove_binop_check [in rt_opt_util]
split1_complete [in list_util]
split1_correct_length [in list_util]
split1_correct_eq [in list_util]
split1_correct [in list_util]
split2_complete [in list_util]
split2_length_ok [in list_util]
split2_correct [in list_util]
split2_equation3 [in list_util]
split2_equation2 [in list_util]
split2_equation1 [in list_util]
storeUpdateRT_completeness [in rt_gen_consistent]
storeUpdateRT_soundness [in rt_gen_consistent]
storeUpdateRT_opt_soundness' [in rt_opt_consistent_util]
storeUpdateRT_opt_completeness' [in rt_opt_consistent_util]
storeUpdateRT_opt_completeness [in rt_opt_consistent_util]
storeUpdateRT_opt_soundness [in rt_opt_consistent_util]
storeUpdate_with_typed_value_preserve_typed_stack [in well_typed_util]
storeUpdate_with_typed_value_preserve_typed_store [in well_typed_util]
store_update_ex_cks_stripped [in eval_rt]
store_update_ex_cks_added [in eval_rt]
STORE.stack_eq_length_trans2 [in environment]
STORE.stack_eq_length_trans [in environment]
STORE.stack_eq_length_sym [in environment]
STORE.stack_eq_length_refl2 [in environment]
STORE.stack_eq_length_refl [in environment]
STORE.updateG_length [in environment]
STORE.updates_length [in environment]
subtype_range_rel_backward [in rt_gen_util]
subtype_range_rel [in rt_gen_util]
sub_bound_unique [in rt_opt_util]
Sub_Bound_Unary_Minus_Compat [in rt_opt_util]
Sub_Bound_Minus_Compat [in rt_opt_util]
Sub_Bound_Plus_Compat [in rt_opt_util]
sub_bound_f_completeness [in rt_opt_impl_consistent]
sub_bound_f_soundness [in rt_opt_impl_consistent]
symbol_table_exp_type_eq [in rt_gen_util]
symbol_table_exp_type_rel [in rt_gen_util]
symbol_table_type_rel_backward [in rt_gen_util]
symbol_table_type_rel [in rt_gen_util]
symbol_table_var_rel [in rt_gen_util]
symbol_table_procedure_rel_backward [in rt_gen_util]
symbol_table_procedure_rel [in rt_gen_util]
T
toArgsRTImpl_completeness [in rt_gen_impl_consistent]toArgsRTImpl_soundness [in rt_gen_impl_consistent]
toAssignStmtRT_completeness [in rt_gen_consistent]
toAssignStmtRT_soundness [in rt_gen_consistent]
toDeclRTConsistent [in rt_gen_consistent]
toDeclRTImpl_completeness [in rt_gen_impl_consistent]
toDeclRTImpl_soundness [in rt_gen_impl_consistent]
toDeclRT_completeness [in rt_gen_consistent]
toDeclRT_soundness [in rt_gen_consistent]
toExpRTConsistent [in rt_gen_consistent]
toExpRTImplConsistent [in rt_gen_impl_consistent]
toExpRTImpl_completeness [in rt_gen_impl_consistent]
toExpRTImpl_soundness [in rt_gen_impl_consistent]
toExpRT_completeness [in rt_gen_consistent]
toExpRT_soundness [in rt_gen_consistent]
toNameRTConsistent [in rt_gen_consistent]
toNameRTImpl_completeness [in rt_gen_impl_consistent]
toNameRTImpl_soundness [in rt_gen_impl_consistent]
toNameRT_completeness [in rt_gen_consistent]
toNameRT_soundness [in rt_gen_consistent]
toObjDeclRTImpl_completeness [in rt_gen_impl_consistent]
toObjDeclRTImpl_soundness [in rt_gen_impl_consistent]
toObjDeclsRTImpl_completeness [in rt_gen_impl_consistent]
toObjDeclsRTImpl_soundness [in rt_gen_impl_consistent]
toParamSpecRTImpl_completeness [in rt_gen_impl_consistent]
toParamSpecRTImpl_soundness [in rt_gen_impl_consistent]
toParamSpecsRTImpl_completeness [in rt_gen_impl_consistent]
toParamSpecsRTImpl_soundness [in rt_gen_impl_consistent]
toProcBodyDeclRTConsistent [in rt_gen_impl_consistent]
toProcBodyDeclRTImpl_completeness [in rt_gen_impl_consistent]
toProcBodyDeclRTImpl_soundness [in rt_gen_impl_consistent]
toProgramRTConsistent [in rt_gen_consistent]
toProgramRTImplConsistent [in rt_gen_impl_consistent]
toProgramRTImpl_completeness [in rt_gen_impl_consistent]
toProgramRTImpl_soundness [in rt_gen_impl_consistent]
toProgramRT_completeness [in rt_gen_consistent]
toProgramRT_soundness [in rt_gen_consistent]
toStmtRTConsistent [in rt_gen_consistent]
toStmtRTImplConsistent [in rt_gen_impl_consistent]
toStmtRTImpl_completeness [in rt_gen_impl_consistent]
toStmtRTImpl_soundness [in rt_gen_impl_consistent]
toStmtRT_completeness [in rt_gen_consistent]
toStmtRT_soundness [in rt_gen_consistent]
toTypeDeclRTImpl_completeness [in rt_gen_impl_consistent]
toTypeDeclRTImpl_soundness [in rt_gen_impl_consistent]
typed_value_in_bound2 [in well_typed_util]
typed_value_in_bound1 [in well_typed_util]
type_match_ref [in well_typed]
type_declaration_rel_backward [in rt_gen_util]
type_declaration_rel [in rt_gen_util]
U
unop_no_check_flagged_soundness [in rt_gen_consistent]unop_no_check_soundness [in rt_gen_consistent]
unop_flagged_overflow_check_soundness [in rt_gen_consistent]
unop_overflow_check_soundness [in rt_gen_consistent]
unop_arithm_operand_format [in eval_rt]
unop_minus_typed [in well_typed_util]
unop_arithm_in_bound [in rt_opt_util]
updated_record_select [in well_typed_util]
updated_array_select [in well_typed_util]
updated_record_select_eq [in well_typed_util]
updated_array_select_eq [in well_typed_util]
updateG_with_typed_value_preserve_typed_stack [in well_typed_util]
update_exterior_checks_name_astnum_eq [in ast_util]
update_exterior_checks_exp_astnum_eq [in ast_util]
V
value_well_typed_with_matched_type [in well_typed_util]value_in_range_is_well_typed [in well_typed_util]
W
wellTypedStatePreservation [in well_typed_util]well_typed_stack_infer [in well_typed]
well_typed_store_infer [in well_typed]
well_typed_value_in_store_fetch [in well_typed_util]
well_typed_int_value_exists [in well_typed_util]
well_typed_value_subtype_trans [in well_typed_util]
well_typed_value_of_var [in well_typed_util]
well_typed_var_in_bound [in well_typed_util]
well_typed_bounded_var_exists_int_value [in well_typed_util]
well_typed_stack_split' [in well_typed_util]
well_typed_store_split' [in well_typed_util]
well_typed_store_stack_split' [in well_typed_util]
well_typed_stacks_merge' [in well_typed_util]
well_typed_store_merge' [in well_typed_util]
well_typed_store_stack_merge' [in well_typed_util]
well_typed_store_updated_by_undefined_value' [in well_typed_util]
well_typed_stacks_merge [in well_typed_util]
well_typed_store_stack_merge [in well_typed_util]
well_typed_store_updated_by_undefined_value [in well_typed_util]
well_typed_name_preserve [in well_typed_util]
well_typed_exp_preserve [in well_typed_util]
Z
Zabs_quot_neg1 [in rt_opt_ZArith]Zabs_ge_neg_v [in rt_opt_ZArith]
Zabs_ge_v [in rt_opt_ZArith]
Zeqb_eq [in rt_opt_ZArith]
Zgele_Bool_Imp_GeLe_F [in rt_opt_ZArith]
Zgele_Bool_Imp_GeLe_T [in rt_opt_ZArith]
Zge_p1_0 [in rt_opt_ZArith]
Zge_le_bool [in rt_opt_ZArith]
Zgt_lt_bool [in rt_opt_ZArith]
Zleb_trans [in rt_opt_ZArith]
Zleb_ltb_trans_ltb [in rt_opt_ZArith]
Zleb_ltb_trans_leb [in rt_opt_ZArith]
Zleb_true_le_true [in rt_opt_ZArith]
Zleb_le [in rt_opt_ZArith]
Zlele_Bool_Imp_LeLe_F [in rt_opt_ZArith]
Zlele_Bool_Imp_LeLe_T [in rt_opt_ZArith]
Zle_n1_0 [in rt_opt_ZArith]
Zle_eq_e_r [in rt_opt_ZArith]
Zle_eq_e_l [in rt_opt_ZArith]
Zle_ge_bool [in rt_opt_ZArith]
Zle_true_leb_true [in rt_opt_ZArith]
Zltb_succ_l [in rt_opt_ZArith]
Zltb_pred_r [in rt_opt_ZArith]
Zltb_trans [in rt_opt_ZArith]
Zltb_leb_trans_ltb [in rt_opt_ZArith]
Zltb_leb_trans_leb [in rt_opt_ZArith]
Zltb_imp_leb [in rt_opt_ZArith]
Zltb_lt [in rt_opt_ZArith]
Zlt_le_pred_r [in rt_opt_ZArith]
Zlt_le_succ_l [in rt_opt_ZArith]
Zlt_le [in rt_opt_ZArith]
Zlt_gt_bool [in rt_opt_ZArith]
Zmult_le_rev_r [in rt_opt_ZArith]
Zmult_le_rev_l [in rt_opt_ZArith]
Zmult_le_ge_l [in rt_opt_ZArith]
Zmult_le_ge_r [in rt_opt_ZArith]
Zmult_lt_lt [in rt_opt_ZArith]
Zmult_le_lt [in rt_opt_ZArith]
Zmult_le_le [in rt_opt_ZArith]
Zquot_n1_interval [in rt_opt_ZArith]
Zquot_p1_interval [in rt_opt_ZArith]
Zquot_n1_opp [in rt_opt_ZArith]
Zquot_n_p_n [in rt_opt_ZArith]
Zquot_p_n_n [in rt_opt_ZArith]
Zquot_n_n_p [in rt_opt_ZArith]
Zquot_p_p_p [in rt_opt_ZArith]
Zquot_le_compat_n_n [in rt_opt_ZArith]
Zquot_le_compat_p_n [in rt_opt_ZArith]
Zquot_le_compat_n_p [in rt_opt_ZArith]
Zquot_le_compat_p_p [in rt_opt_ZArith]
Zquot_antitone [in rt_opt_ZArith]
Axiom Index
E
ENTRY.T [in environment]S
SymTable_Element.Source_Location [in symboltable_module]SymTable_Element.Type_Decl [in symboltable_module]
SymTable_Element.Procedure_Decl [in symboltable_module]
Projection Index
A
anno [in rt_validator]annotation [in rt_validator]
astNumber [in rt_validator]
ast_number [in rt_validator]
C
col [in symboltable]D
declaration_astnum [in ast]declaration_astnum_rt [in ast_rt]
decls [in ast]
declsRT [in ast_rt]
division_cks [in rt_counter]
E
endcol [in symboltable]endline [in symboltable]
expectedCompleteChecks [in rt_validator]
expectedOptimizedChecks [in rt_validator]
expected_complete_checks [in rt_validator]
expected_optimized_checks [in rt_validator]
G
gnatproChecks [in rt_validator]gnatpro_checks [in rt_validator]
I
initialization_exp [in ast]initialization_expRT [in ast_rt]
L
line [in symboltable]M
main [in ast]mainRT [in ast_rt]
N
num_of_cks [in rt_counter]O
object_nominal_subtype [in ast]object_name [in ast]
object_nominal_subtype_rt [in ast_rt]
object_nameRT [in ast_rt]
overflow_cks [in rt_counter]
P
parameter_mode [in ast]parameter_subtype_mark [in ast]
parameter_name [in ast]
parameter_astnum [in ast]
parameter_mode_rt [in ast_rt]
parameter_subtype_mark_rt [in ast_rt]
parameter_nameRT [in ast_rt]
parameter_astnum_rt [in ast_rt]
pkgNames [in symboltable_module]
procNames [in symboltable_module]
R
range_cks [in rt_counter]S
sourceLoc [in rt_validator]SymbolTableM.exps [in symboltable_module]
SymbolTableM.names [in symboltable_module]
SymbolTableM.procs [in symboltable_module]
SymbolTableM.sloc [in symboltable_module]
SymbolTableM.types [in symboltable_module]
SymbolTableM.vars [in symboltable_module]
T
typeNames [in symboltable_module]V
varNames [in symboltable_module]Inductive Index
B
binary_operator [in ast_basics]bound [in values]
C
check_flag [in rt]copyIn [in eval]
copyInRT [in eval_rt]
copyOut [in eval]
copyOutRT [in eval_rt]
cutUntil [in eval]
D
decl [in ast]declRT [in ast_rt]
diff_annotation [in rt_validator]
divCheck [in eval]
do_run_time_check_on_unop [in eval]
do_run_time_check_on_binop [in eval]
E
errorType [in values]evalBinOpRT [in eval_rt]
evalBinOpRTS [in eval_rt]
evalDecl [in eval]
evalDeclRT [in eval_rt]
evalExp [in eval]
evalExpRT [in eval_rt]
evalLiteral [in eval]
evalLiteralRT [in eval_rt]
evalName [in eval]
evalNameRT [in eval_rt]
evalProgram [in eval]
evalProgramRT [in eval_rt]
evalStmt [in eval]
evalStmtRT [in eval_rt]
evalUnOpRT [in eval_rt]
evalUnOpRTS [in eval_rt]
exp [in ast]
expRT [in ast_rt]
extract_array_index_range_rt [in symboltable]
extract_subtype_range_rt [in symboltable]
extract_array_index_range [in symboltable]
extract_subtype_range [in symboltable]
I
in_bound [in values]L
literal [in ast_basics]M
mode [in ast_basics]N
name [in ast]nameRT [in ast_rt]
O
overflowCheck [in eval]overflowChecks [in eval_rt]
P
procBodyDecl [in ast]procBodyDeclRT [in ast_rt]
R
range [in ast]rangeCheck [in eval]
rangeChecks [in eval_rt]
rangeRT [in ast_rt]
Ret [in values]
return_message' [in rt_validator]
return_message [in rt_validator]
S
stmt [in ast]stmtRT [in ast_rt]
storeUpdate [in eval]
storeUpdateRT [in eval_rt]
STORE.stack_eq_length [in environment]
T
toArgsRT [in rt_gen]toDeclRT [in rt_gen]
toExpRT [in rt_gen]
toNameRT [in rt_gen]
toObjDeclRT [in rt_gen]
toObjDeclsRT [in rt_gen]
toParamSpecRT [in rt_gen]
toParamSpecsRT [in rt_gen]
toProcBodyDeclRT [in rt_gen]
toProcDeclRTMap [in rt_gen_util]
toProgramRT [in rt_gen]
toStmtRT [in rt_gen]
toSymTabRT [in rt_gen_util]
toTypeDeclRT [in rt_gen]
toTypeDeclRTMap [in rt_gen_util]
type [in ast_basics]
typeDecl [in ast]
typeDeclRT [in ast_rt]
U
unary_operator [in ast_basics]V
value [in values]W
well_typed_stack_and_symboltable [in well_typed]well_typed_value_in_stack [in well_typed]
well_typed_stack [in well_typed]
well_typed_value_in_store [in well_typed]
well_typed_store [in well_typed]
well_typed_value [in well_typed]
well_typed_symbol_table [in well_typed]
well_typed_proc_declaration [in well_typed]
well_typed_subtype_declaration [in well_typed]
well_typed_program_x [in well_typed]
well_typed_proc_body_x [in well_typed]
well_typed_decl_x [in well_typed]
well_typed_type_decl_x [in well_typed]
well_typed_statement_x [in well_typed]
well_typed_args_x [in well_typed]
well_typed_params_x [in well_typed]
well_typed_exps_x [in well_typed]
well_typed_name_x [in well_typed]
well_typed_exp_x [in well_typed]
Section Index
A
AuxiliaryFunctions [in ast]AuxiliaryFunctions_For_AST_RT [in ast_util]
AuxiliaryFunctions_For_AST [in ast_util]
AuxiliaryFunctions_RT [in ast_rt]
C
Checks_Generator_Implementation_Completeness_Proof [in rt_gen_impl_consistent]Checks_Generator_Implementation_Soundness_Proof [in rt_gen_impl_consistent]
Check_Count [in rt_counter]
Check_Flags_Validator [in rt_validator]
L
LB_AuxiliaryFunctions [in ast_basics]M
Map_To_Source_Location [in rt_validator]Abbreviation Index
S
STORE.V [in environment]Definition Index
A
arrindex [in ast_basics]astnum [in ast_basics]
B
beq_type [in ast_basics]binop_type [in well_typed]
C
checks_validator [in rt_validator]check_flags [in rt]
count_option_declaration_check_flags [in rt_counter]
D
declaration_ind [in rt_gen_impl_consistent]declaration_x_ind [in rt_opt_impl_consistent]
Division_Error [in values]
done [in CpdtTactics]
E
Entry_Value_Stored.T [in eval]expression_astnum [in ast]
expression_ind [in rt_gen_consistent]
expression_x_ind [in eval_rt]
expression_ind [in eval_rt]
expression_x_ind [in rt_opt_consistent]
expression_ind [in rt_opt_consistent]
expression_x_ind [in rt_opt_util]
expression_ind [in rt_opt_util]
expression_x_ind [in rt_opt_consistent_util]
expression_ind [in rt_opt_consistent_util]
expression_astnum_rt [in ast_rt]
expression_ind [in rt_gen_impl_consistent]
expression_x_ind [in rt_opt_impl_consistent]
exterior_checks [in rt]
F
fetch_array_index_type_rt [in symboltable]fetch_array_index_type [in symboltable]
fetch_sloc_rt [in symboltable]
fetch_exp_type_rt [in symboltable]
fetch_type_rt [in symboltable]
fetch_proc_rt [in symboltable]
fetch_var_rt [in symboltable]
fetch_type_name_rt [in symboltable]
fetch_pkg_name_rt [in symboltable]
fetch_proc_name_rt [in symboltable]
fetch_var_name_rt [in symboltable]
fetch_sloc [in symboltable]
fetch_exp_type [in symboltable]
fetch_type [in symboltable]
fetch_proc [in symboltable]
fetch_var [in symboltable]
fetch_type_name [in symboltable]
fetch_pkg_name [in symboltable]
fetch_proc_name [in symboltable]
fetch_var_name [in symboltable]
H
half_modulus [in values]I
idnum [in ast_basics]interior_checks [in rt]
int32_bound [in values]
is_in_out_mode [in ast_basics]
is_out_mode [in ast_basics]
is_in_mode [in ast_basics]
is_range_constrainted_type [in ast_basics]
L
level [in symboltable]M
map_to_source_location [in rt_validator]Math.add [in values]
Math.and [in values]
Math.binary_operation [in values]
Math.div [in values]
Math.eq [in values]
Math.ge [in values]
Math.gt [in values]
Math.le [in values]
Math.lt [in values]
Math.mod' [in values]
Math.mul [in values]
Math.ne [in values]
Math.or [in values]
Math.rem [in values]
Math.sub [in values]
Math.unary_operation [in values]
Math.unary_minus [in values]
Math.unary_plus [in values]
Math.unary_not [in values]
max_signed [in values]
max_unsigned [in values]
min_signed [in values]
mkSymTab [in symboltable]
mkSymTabRT [in symboltable]
modulus [in values]
N
name_astnum [in ast]name_ind [in rt_gen_consistent]
name_x_ind [in eval_rt]
name_ind [in eval_rt]
name_x_ind [in rt_opt_consistent]
name_ind [in rt_opt_consistent]
name_x_ind [in rt_opt_util]
name_ind [in rt_opt_util]
name_x_ind [in rt_opt_consistent_util]
name_ind [in rt_opt_consistent_util]
name_astnum_rt [in ast_rt]
name_ind [in rt_gen_impl_consistent]
name_x_ind [in rt_opt_impl_consistent]
O
Overflow_Error [in values]P
pkgnum [in ast_basics]procedure_name [in ast]
procedure_parameter_profile [in ast]
procedure_declarative_part [in ast]
procedure_statements [in ast]
procedure_parameter_profile_rt [in ast_rt]
procedure_declarative_part_rt [in ast_rt]
procedure_statements_rt [in ast_rt]
procedure_body_ind [in rt_gen_impl_consistent]
procedure_body_x_ind [in rt_opt_impl_consistent]
procedur_name_rt [in ast_rt]
procnum [in ast_basics]
proc_decl_rt [in symboltable]
proc_decl [in symboltable]
program_checks_validator [in rt_validator]
R
Range_Error [in values]reside_symtable_sloc_rt [in symboltable]
reside_symtable_exps_rt [in symboltable]
reside_symtable_types_rt [in symboltable]
reside_symtable_procs_rt [in symboltable]
reside_symtable_vars_rt [in symboltable]
reside_nametable_types_rt [in symboltable]
reside_nametable_pkgs_rt [in symboltable]
reside_nametable_procs_rt [in symboltable]
reside_nametable_vars_rt [in symboltable]
reside_symtable_sloc [in symboltable]
reside_symtable_exps [in symboltable]
reside_symtable_types [in symboltable]
reside_symtable_procs [in symboltable]
reside_symtable_vars [in symboltable]
reside_nametable_types [in symboltable]
reside_nametable_pkgs [in symboltable]
reside_nametable_procs [in symboltable]
reside_nametable_vars [in symboltable]
S
STORE.cut_to [in environment]STORE.fetch [in environment]
STORE.frame [in environment]
STORE.level_of [in environment]
STORE.newFrame [in environment]
STORE.push [in environment]
STORE.pushG [in environment]
STORE.reside [in environment]
STORE.scope_level [in environment]
STORE.state [in environment]
STORE.store [in environment]
STORE.store_of [in environment]
STORE.update [in environment]
subtype_range [in ast]
subtype_num [in ast_basics]
subtype_range_rt [in ast_rt]
SymbolTableM.Entry_Sloc.T [in symboltable_module]
SymbolTableM.Entry_Exp_Type.T [in symboltable_module]
SymbolTableM.Entry_Type_Decl.T [in symboltable_module]
SymbolTableM.Entry_Procedure_Decl.T [in symboltable_module]
SymbolTableM.Entry_Type.T [in symboltable_module]
SymbolTableM.Entry_Name.T [in symboltable_module]
SymbolTableM.level [in symboltable_module]
SymbolTableM.proc_decl [in symboltable_module]
SymbolTableM.source_location [in symboltable_module]
SymbolTableM.type_decl [in symboltable_module]
Symbol_Table_Elements_RT.Source_Location [in symboltable]
Symbol_Table_Elements_RT.Type_Decl [in symboltable]
Symbol_Table_Elements_RT.Procedure_Decl [in symboltable]
Symbol_Table_Elements.Source_Location [in symboltable]
Symbol_Table_Elements.Type_Decl [in symboltable]
Symbol_Table_Elements.Procedure_Decl [in symboltable]
symTab [in symboltable]
symTabRT [in symboltable]
T
typenum [in ast_basics]type_name [in ast]
type_match [in well_typed]
type_of_exp_x [in well_typed]
type_of_name_x [in well_typed]
type_name_rt [in ast_rt]
type_decl_rt [in symboltable]
type_decl [in symboltable]
U
unop_type [in well_typed]update_exterior_checks_exp [in ast_util]
update_exterior_checks_name [in ast_util]
update_sloc_rt [in symboltable]
update_exps_rt [in symboltable]
update_types_rt [in symboltable]
update_procs_rt [in symboltable]
update_vars_rt [in symboltable]
update_sloc [in symboltable]
update_exps [in symboltable]
update_types [in symboltable]
update_procs [in symboltable]
update_vars [in symboltable]
W
wordsize [in values]Record Index
C
cks_infor_t [in rt_counter]D
diff_message' [in rt_validator]diff_message [in rt_validator]
N
nametable [in symboltable_module]O
objDecl [in ast]objDeclRT [in ast_rt]
P
paramSpec [in ast]paramSpecRT [in ast_rt]
program [in ast]
programRT [in ast_rt]
S
source_location [in symboltable]SymbolTableM.symboltable [in symboltable_module]
| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1197 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (23 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (29 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (397 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (390 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (4 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (49 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (97 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (10 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (185 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (12 entries) |
This page has been generated by coqdoc