Skip to content

Commit 169f177

Browse files
tjj2017tjj2017
committed
Merge branch 'translate_withed_units_once_only' of https://github.com/tjj2017/gnat2goto into translate_withed_units_once_only
2 parents f5d2aec + 9ff6cfe commit 169f177

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

48 files changed

+1138
-181
lines changed

‎experiments/golden-results/StratoX-summary.txt

Lines changed: 25 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -8,16 +8,11 @@ Calling function: Process_Pragma_Declaration
88
Error message: Unsupported pragma: Precondition
99
Nkind: N_Pragma
1010
--
11-
Occurs: 232 times
11+
Occurs: 231 times
1212
Calling function: Process_Declaration
1313
Error message: Unknown declaration kind
1414
Nkind: N_Validate_Unchecked_Conversion
1515
--
16-
Occurs: 202 times
17-
Calling function: Process_Pragma_Declaration
18-
Error message: Unsupported pragma: Suppress initialization
19-
Nkind: N_Pragma
20-
--
2116
Occurs: 152 times
2217
Calling function: Process_Pragma_Declaration
2318
Error message: Unsupported pragma: Postcondition
@@ -184,6 +179,11 @@ Error message: Unsupported pragma: Refine
184179
Nkind: N_Pragma
185180
--
186181
Occurs: 1 times
182+
Calling function: Process_Pragma_Declaration
183+
Error message: Unsupported pragma: Suppress initialization
184+
Nkind: N_Pragma
185+
--
186+
Occurs: 1 times
187187
Calling function: Process_Statement
188188
Error message: Unknown expression kind
189189
Nkind: N_Object_Renaming_Declaration
@@ -1750,12 +1750,17 @@ Error detected at REDACTED
17501750
--
17511751
Occurs: 1 times
17521752
+===========================GNAT BUG DETECTED==============================+
1753-
| GNU Ada (ada2goto) Assert_Failure failed precondition from arrays.ads:51 |
1753+
| GNU Ada (ada2goto) Assert_Failure atree.adb:992 |
17541754
Error detected at REDACTED
17551755
--
17561756
Occurs: 1 times
17571757
+===========================GNAT BUG DETECTED==============================+
1758-
| GNU Ada (ada2goto) Assert_Failure failed precondition from arrays.ads:51 |
1758+
| GNU Ada (ada2goto) Assert_Failure failed precondition from arrays.ads:71 |
1759+
Error detected at REDACTED
1760+
--
1761+
Occurs: 1 times
1762+
+===========================GNAT BUG DETECTED==============================+
1763+
| GNU Ada (ada2goto) Assert_Failure failed precondition from arrays.ads:71 |
17591764
Error detected at REDACTED
17601765
--
17611766
Occurs: 1 times
@@ -2105,52 +2110,52 @@ Error detected at REDACTED
21052110
--
21062111
Occurs: 1 times
21072112
+===========================GNAT BUG DETECTED==============================+
2108-
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:54|
2113+
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:55|
21092114
Error detected at REDACTED
21102115
--
21112116
Occurs: 1 times
21122117
+===========================GNAT BUG DETECTED==============================+
2113-
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:54|
2118+
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:55|
21142119
Error detected at REDACTED
21152120
--
21162121
Occurs: 1 times
21172122
+===========================GNAT BUG DETECTED==============================+
2118-
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:54|
2123+
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:55|
21192124
Error detected at REDACTED
21202125
--
21212126
Occurs: 1 times
21222127
+===========================GNAT BUG DETECTED==============================+
2123-
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:54|
2128+
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:55|
21242129
Error detected at REDACTED
21252130
--
21262131
Occurs: 1 times
21272132
+===========================GNAT BUG DETECTED==============================+
2128-
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:54|
2133+
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:55|
21292134
Error detected at REDACTED
21302135
--
21312136
Occurs: 1 times
21322137
+===========================GNAT BUG DETECTED==============================+
2133-
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:54|
2138+
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:55|
21342139
Error detected at REDACTED
21352140
--
21362141
Occurs: 1 times
21372142
+===========================GNAT BUG DETECTED==============================+
2138-
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:54|
2143+
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:55|
21392144
Error detected at REDACTED
21402145
--
21412146
Occurs: 1 times
21422147
+===========================GNAT BUG DETECTED==============================+
2143-
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:54|
2148+
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:55|
21442149
Error detected at REDACTED
21452150
--
21462151
Occurs: 1 times
21472152
+===========================GNAT BUG DETECTED==============================+
2148-
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:54|
2153+
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:55|
21492154
Error detected at REDACTED
21502155
--
21512156
Occurs: 1 times
21522157
+===========================GNAT BUG DETECTED==============================+
2153-
| GNU Ada (ada2goto) Assert_Failure failed precondition from tree_walk.adb:72|
2158+
| GNU Ada (ada2goto) Assert_Failure failed precondition from tree_walk.adb:71|
21542159
Error detected at REDACTED
21552160
--
21562161
Occurs: 1 times
@@ -2192,11 +2197,6 @@ Occurs: 25 times
21922197
<========================>
21932198
raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : failed precondition from goto_utils.ads:147
21942199

2195-
--
2196-
Occurs: 4 times
2197-
<========================>
2198-
raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : failed precondition from arrays.ads:57
2199-
22002200
--
22012201
Occurs: 2 times
22022202
<========================>
@@ -2205,10 +2205,10 @@ raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : failed precondition from arrays.ads:51
22052205
--
22062206
Occurs: 2 times
22072207
<========================>
2208-
raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : failed precondition from range_check.ads:54
2208+
raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : failed precondition from range_check.ads:55
22092209

22102210
--
22112211
Occurs: 1 times
22122212
<========================>
2213-
raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : failed precondition from tree_walk.adb:72
2213+
raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : failed precondition from tree_walk.adb:71
22142214

‎experiments/golden-results/Tokeneer-summary.txt

Lines changed: 4 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,3 @@
1-
Occurs: 21 times
2-
Calling function: Process_Pragma_Declaration
3-
Error message: Unsupported pragma: Suppress initialization
4-
Nkind: N_Pragma
5-
--
61
Occurs: 9 times
72
Calling function: Do_Aggregate_Literal
83
Error message: Unhandled aggregate kind: E_PRIVATE_TYPE
@@ -1035,7 +1030,7 @@ Error detected at REDACTED
10351030
--
10361031
Occurs: 2 times
10371032
+===========================GNAT BUG DETECTED==============================+
1038-
| GNU Ada (ada2goto) Assert_Failure failed precondition from tree_walk.ads:105|
1033+
| GNU Ada (ada2goto) Assert_Failure failed precondition from tree_walk.ads:108|
10391034
Error detected at REDACTED
10401035
--
10411036
Occurs: 1 times
@@ -1105,17 +1100,17 @@ Error detected at REDACTED
11051100
--
11061101
Occurs: 1 times
11071102
+===========================GNAT BUG DETECTED==============================+
1108-
| GNU Ada (ada2goto) Assert_Failure failed precondition from tree_walk.ads:105|
1103+
| GNU Ada (ada2goto) Assert_Failure failed precondition from tree_walk.ads:108|
11091104
Error detected at REDACTED
11101105
--
11111106
Occurs: 1 times
11121107
+===========================GNAT BUG DETECTED==============================+
1113-
| GNU Ada (ada2goto) Assert_Failure failed precondition from tree_walk.ads:105|
1108+
| GNU Ada (ada2goto) Assert_Failure failed precondition from tree_walk.ads:108|
11141109
Error detected at REDACTED
11151110
--
11161111
Occurs: 1 times
11171112
+===========================GNAT BUG DETECTED==============================+
1118-
| GNU Ada (ada2goto) Assert_Failure failed precondition from tree_walk.ads:105|
1113+
| GNU Ada (ada2goto) Assert_Failure failed precondition from tree_walk.ads:108|
11191114
Error detected at REDACTED
11201115
--
11211116
Occurs: 1 times

‎experiments/golden-results/ksum-summary.txt

Lines changed: 0 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,3 @@
1-
Occurs: 3 times
2-
Calling function: Process_Pragma_Declaration
3-
Error message: Unsupported pragma: Suppress initialization
4-
Nkind: N_Pragma
5-
--
61
Occurs: 41 times
72
Redacted compiler error message:
83
file "REDACTED" not found

‎experiments/golden-results/libkeccak-summary.txt

Lines changed: 25 additions & 30 deletions
Original file line numberDiff line numberDiff line change
@@ -18,11 +18,6 @@ Calling function: Process_Declaration
1818
Error message: Use type clause declaration
1919
Nkind: N_Use_Type_Clause
2020
--
21-
Occurs: 18 times
22-
Calling function: Process_Pragma_Declaration
23-
Error message: Unsupported pragma: Suppress initialization
24-
Nkind: N_Pragma
25-
--
2621
Occurs: 2 times
2722
Calling function: Do_Expression
2823
Error message: ATTRIBUTE_ASM_OUTPUT unsupported
@@ -35,7 +30,7 @@ Raw compiler error message:
3530
--
3631
Occurs: 23 times
3732
+===========================GNAT BUG DETECTED==============================+
38-
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:54|
33+
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:55|
3934
Error detected at REDACTED
4035
--
4136
Occurs: 2 times
@@ -45,122 +40,122 @@ Error detected at REDACTED
4540
--
4641
Occurs: 1 times
4742
+===========================GNAT BUG DETECTED==============================+
48-
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:54|
43+
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:55|
4944
Error detected at REDACTED
5045
--
5146
Occurs: 1 times
5247
+===========================GNAT BUG DETECTED==============================+
53-
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:54|
48+
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:55|
5449
Error detected at REDACTED
5550
--
5651
Occurs: 1 times
5752
+===========================GNAT BUG DETECTED==============================+
58-
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:54|
53+
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:55|
5954
Error detected at REDACTED
6055
--
6156
Occurs: 1 times
6257
+===========================GNAT BUG DETECTED==============================+
63-
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:54|
58+
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:55|
6459
Error detected at REDACTED
6560
--
6661
Occurs: 1 times
6762
+===========================GNAT BUG DETECTED==============================+
68-
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:54|
63+
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:55|
6964
Error detected at REDACTED
7065
--
7166
Occurs: 1 times
7267
+===========================GNAT BUG DETECTED==============================+
73-
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:54|
68+
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:55|
7469
Error detected at REDACTED
7570
--
7671
Occurs: 1 times
7772
+===========================GNAT BUG DETECTED==============================+
78-
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:54|
73+
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:55|
7974
Error detected at REDACTED
8075
--
8176
Occurs: 1 times
8277
+===========================GNAT BUG DETECTED==============================+
83-
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:54|
78+
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:55|
8479
Error detected at REDACTED
8580
--
8681
Occurs: 1 times
8782
+===========================GNAT BUG DETECTED==============================+
88-
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:54|
83+
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:55|
8984
Error detected at REDACTED
9085
--
9186
Occurs: 1 times
9287
+===========================GNAT BUG DETECTED==============================+
93-
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:54|
88+
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:55|
9489
Error detected at REDACTED
9590
--
9691
Occurs: 1 times
9792
+===========================GNAT BUG DETECTED==============================+
98-
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:54|
93+
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:55|
9994
Error detected at REDACTED
10095
--
10196
Occurs: 1 times
10297
+===========================GNAT BUG DETECTED==============================+
103-
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:54|
98+
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:55|
10499
Error detected at REDACTED
105100
--
106101
Occurs: 1 times
107102
+===========================GNAT BUG DETECTED==============================+
108-
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:54|
103+
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:55|
109104
Error detected at REDACTED
110105
--
111106
Occurs: 1 times
112107
+===========================GNAT BUG DETECTED==============================+
113-
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:54|
108+
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:55|
114109
Error detected at REDACTED
115110
--
116111
Occurs: 1 times
117112
+===========================GNAT BUG DETECTED==============================+
118-
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:54|
113+
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:55|
119114
Error detected at REDACTED
120115
--
121116
Occurs: 1 times
122117
+===========================GNAT BUG DETECTED==============================+
123-
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:54|
118+
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:55|
124119
Error detected at REDACTED
125120
--
126121
Occurs: 1 times
127122
+===========================GNAT BUG DETECTED==============================+
128-
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:54|
123+
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:55|
129124
Error detected at REDACTED
130125
--
131126
Occurs: 1 times
132127
+===========================GNAT BUG DETECTED==============================+
133-
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:54|
128+
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:55|
134129
Error detected at REDACTED
135130
--
136131
Occurs: 1 times
137132
+===========================GNAT BUG DETECTED==============================+
138-
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:54|
133+
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:55|
139134
Error detected at REDACTED
140135
--
141136
Occurs: 1 times
142137
+===========================GNAT BUG DETECTED==============================+
143-
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:54|
138+
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:55|
144139
Error detected at REDACTED
145140
--
146141
Occurs: 1 times
147142
+===========================GNAT BUG DETECTED==============================+
148-
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:54|
143+
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:55|
149144
Error detected at REDACTED
150145
--
151146
Occurs: 1 times
152147
+===========================GNAT BUG DETECTED==============================+
153-
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:54|
148+
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:55|
154149
Error detected at REDACTED
155150
--
156151
Occurs: 1 times
157152
+===========================GNAT BUG DETECTED==============================+
158-
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:54|
153+
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:55|
159154
Error detected at REDACTED
160155
--
161156
Occurs: 1 times
162157
+===========================GNAT BUG DETECTED==============================+
163-
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:54|
158+
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:55|
164159
Error detected at REDACTED
165160
--
166161
Occurs: 1 times

‎experiments/golden-results/libsparkcrypto-summary.txt

Lines changed: 0 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -83,11 +83,6 @@ Calling function: Do_Expression
8383
Error message: ATTRIBUTE_ASM_OUTPUT unsupported
8484
Nkind: N_Attribute_Reference
8585
--
86-
Occurs: 2 times
87-
Calling function: Process_Pragma_Declaration
88-
Error message: Known but unsupported pragma: Linker Options
89-
Nkind: N_Pragma
90-
--
9186
Occurs: 32 times
9287
Redacted compiler error message:
9388
file "REDACTED" not found

‎experiments/golden-results/muen-summary.txt

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3175,7 +3175,7 @@ Error detected at REDACTED
31753175
--
31763176
Occurs: 1 times
31773177
+===========================GNAT BUG DETECTED==============================+
3178-
| GNU Ada (ada2goto) Assert_Failure failed precondition from tree_walk.ads:105|
3178+
| GNU Ada (ada2goto) Assert_Failure failed precondition from tree_walk.ads:108|
31793179
Error detected at REDACTED
31803180
--
31813181
Occurs: 1 times

‎experiments/golden-results/vct-summary.txt

Lines changed: 1 addition & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -18,11 +18,6 @@ Calling function: Do_Expression
1818
Error message: ATTRIBUTE_COPY_SIGN unsupported
1919
Nkind: N_Attribute_Reference
2020
--
21-
Occurs: 6 times
22-
Calling function: Process_Pragma_Declaration
23-
Error message: Unsupported pragma: Suppress initialization
24-
Nkind: N_Pragma
25-
--
2621
Occurs: 4 times
2722
Calling function: Process_Declaration
2823
Error message: size clause not applied by the front-end
@@ -310,5 +305,5 @@ Error detected at REDACTED
310305
--
311306
Occurs: 2 times
312307
<========================>
313-
raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : failed precondition from range_check.ads:54
308+
raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : failed precondition from range_check.ads:55
314309

0 commit comments

Comments
 (0)