1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
|
-------------------------------------------------------------------------------
-- (C) Altran Praxis Limited
-------------------------------------------------------------------------------
--
-- The SPARK toolset is free software; you can redistribute it and/or modify it
-- under terms of the GNU General Public License as published by the Free
-- Software Foundation; either version 3, or (at your option) any later
-- version. The SPARK toolset is distributed in the hope that it will be
-- useful, but WITHOUT ANY WARRANTY; without even the implied warranty of
-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General
-- Public License for more details. You should have received a copy of the GNU
-- General Public License distributed with the SPARK toolset; see file
-- COPYING3. If not, go to http://www.gnu.org/licenses for a complete copy of
-- the license.
--
--=============================================================================
--# inherit ScreenEcho,
--# SPARK_IO,
--# Version;
package SystemErrors is
type Sys_Err_Type is (String_Table_Overflow,
Syntax_Tree_Overflow,
Parse_Stack_Overflow,
Symbol_Table_Overflow_Dynamic,
Invalid_Syntax_Tree,
Invalid_Symbol_Table,
Empty_Heap,
Relation_Stack_Underflow,
Relation_Stack_Overflow,
Invalid_Init,
Error_Position_Wrong,
Expression_Stack_Corrupt,
Expression_Stack_Underflow,
Expression_Stack_Overflow,
Type_Context_Stack_Corrupt,
Type_Context_Stack_Underflow,
Type_Context_Stack_Overflow,
List_Overflow_In_Expression,
List_Overflow_In_Dependency_Clause,
List_Overflow_In_Procedure_Call,
Case_Stack_Underflow,
Case_Stack_Overflow,
VCG_Graph_Size_Exceeded,
VCG_Heap_Is_Exhausted,
VCG_Heap_Is_Corrupted,
Ref_List_Key_Cell_Missing,
Flow_Analyser_Expression_Limit,
Case_Statement_Nesting_Limit,
Error_Handler_Temporary_Files,
Error_Handler_Source,
Disk_Full_Error,
Math_Error,
Too_Many_Nested_Arrays,
Too_Many_Nested_Records,
Context_Unit_Stack_Overflow,
Context_Unit_Stack_Underflow,
Context_File_Heap_Overflow,
Context_Unit_Heap_Overflow,
Too_Many_File_Lines,
Index_Stack_Full,
Index_Component_List_Full,
Too_Many_Errors,
Warning_Name_Too_Long,
Unit_Name_In_Index_Too_Long,
File_Name_In_Index_Too_Long,
Too_Many_Suppressed_Warnings,
Unit_Nesting_Too_Deep,
Statement_Stack_Underflow,
Statement_Stack_Overflow,
Wf_Compilation_Unit_Stack_Overflow,
Wf_Compilation_Unit_Stack_Underflow,
Too_Many_Flow_Analyser_Expressions,
Too_Many_Params_In_Procedure_Call,
Statistics_Usage_Greater_Than_Table_Size,
Aggregate_Stack_Under_Flow,
Aggregate_Stack_Over_Flow,
Meta_File_Stack_Overflow,
Lex_Stack_Overflow,
Lex_Stack_Underflow,
Component_Manager_Overflow,
Component_Error_Overflow,
Syntax_Tree_Walk_Error,
Precondition_Failure,
Postcondition_Failure,
Assertion_Failure,
Unimplemented_Feature,
XML_Schema_Error,
XML_Generation_Error,
Illegal_XML_Generation_Attempt,
String_Over_Flow,
Queue_Overflow,
XRef_Table_Full,
Invalid_Index,
-- Add additional specific entries here...
Other_Internal_Error);
-- Proof function can be asserted true and, on paths where SystemErrors is called
-- this will appear in hypotheses; this helps understand what is going on.
--# function Halted return Boolean;
-- Raises Sys_Err with Msg
procedure Fatal_Error (Sys_Err : in Sys_Err_Type;
Msg : in String);
--# derives null from Msg,
--# Sys_Err;
--# post Halted and -- this helps us understand VCs where SystemError called
--# False; -- this ensures that such paths are provable by contradiction
-- if C if False, then Raises Sys_Err with Msg
-- if C is True, then returns
procedure RT_Assert (C : in Boolean;
Sys_Err : in Sys_Err_Type;
Msg : in String);
--# derives null from C,
--# Msg,
--# Sys_Err;
--# post C or (not C and Halted and False);
-- This routine is intended to signal "interesting" but non-critical
-- assertions in the Examiner - things that should be True, but if
-- False we should know about but don't prevent the Examiner from
-- carrying on or the validity of any subsequent analyses.
--
-- If C is False, then print Msg to Standard_Output and carry on
-- If C is True, then no action and returns
procedure RT_Warning (C : in Boolean;
Msg : in String);
--# derives null from C,
--# Msg;
end SystemErrors;
|
