Skip to content

Commit 033dd7e

Browse files
tjj2017tjj2017
committed
Update test results and resolve conflicts.
Merge branch 'iss_131_ready' of https://github.com/tjj2017/gnat2goto into iss_131_ready
2 parents 55eb475 + 235de82 commit 033dd7e

Some content is hidden

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

50 files changed

+1108
-290
lines changed

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

Lines changed: 23 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -3,16 +3,11 @@ Calling function: Process_Pragma_Declaration
33
Error message: Unsupported pragma: Precondition
44
Nkind: N_Pragma
55
--
6-
Occurs: 232 times
6+
Occurs: 231 times
77
Calling function: Process_Declaration
88
Error message: Unknown declaration kind
99
Nkind: N_Validate_Unchecked_Conversion
1010
--
11-
Occurs: 202 times
12-
Calling function: Process_Pragma_Declaration
13-
Error message: Unsupported pragma: Suppress initialization
14-
Nkind: N_Pragma
15-
--
1611
Occurs: 153 times
1712
Calling function: Process_Pragma_Declaration
1813
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
@@ -1755,12 +1755,17 @@ 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 atree.adb:992 |
17591759
Error detected at REDACTED
17601760
--
17611761
Occurs: 1 times
17621762
+===========================GNAT BUG DETECTED==============================+
1763-
| GNU Ada (ada2goto) Assert_Failure failed precondition from arrays.ads:51 |
1763+
| GNU Ada (ada2goto) Assert_Failure failed precondition from arrays.ads:71 |
1764+
Error detected at REDACTED
1765+
--
1766+
Occurs: 1 times
1767+
+===========================GNAT BUG DETECTED==============================+
1768+
| GNU Ada (ada2goto) Assert_Failure failed precondition from arrays.ads:71 |
17641769
Error detected at REDACTED
17651770
--
17661771
Occurs: 1 times
@@ -1780,47 +1785,47 @@ Error detected at REDACTED
17801785
--
17811786
Occurs: 1 times
17821787
+===========================GNAT BUG DETECTED==============================+
1783-
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:54|
1788+
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:55|
17841789
Error detected at REDACTED
17851790
--
17861791
Occurs: 1 times
17871792
+===========================GNAT BUG DETECTED==============================+
1788-
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:54|
1793+
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:55|
17891794
Error detected at REDACTED
17901795
--
17911796
Occurs: 1 times
17921797
+===========================GNAT BUG DETECTED==============================+
1793-
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:54|
1798+
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:55|
17941799
Error detected at REDACTED
17951800
--
17961801
Occurs: 1 times
17971802
+===========================GNAT BUG DETECTED==============================+
1798-
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:54|
1803+
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:55|
17991804
Error detected at REDACTED
18001805
--
18011806
Occurs: 1 times
18021807
+===========================GNAT BUG DETECTED==============================+
1803-
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:54|
1808+
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:55|
18041809
Error detected at REDACTED
18051810
--
18061811
Occurs: 1 times
18071812
+===========================GNAT BUG DETECTED==============================+
1808-
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:54|
1813+
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:55|
18091814
Error detected at REDACTED
18101815
--
18111816
Occurs: 1 times
18121817
+===========================GNAT BUG DETECTED==============================+
1813-
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:54|
1818+
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:55|
18141819
Error detected at REDACTED
18151820
--
18161821
Occurs: 1 times
18171822
+===========================GNAT BUG DETECTED==============================+
1818-
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:54|
1823+
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:55|
18191824
Error detected at REDACTED
18201825
--
18211826
Occurs: 1 times
18221827
+===========================GNAT BUG DETECTED==============================+
1823-
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:54|
1828+
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:55|
18241829
Error detected at REDACTED
18251830
--
18261831
Occurs: 1 times
@@ -2217,11 +2222,6 @@ Occurs: 25 times
22172222
<========================>
22182223
raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : failed precondition from goto_utils.ads:147
22192224

2220-
--
2221-
Occurs: 4 times
2222-
<========================>
2223-
raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : failed precondition from arrays.ads:57
2224-
22252225
--
22262226
Occurs: 2 times
22272227
<========================>
@@ -2235,7 +2235,7 @@ raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : failed precondition from arrays.ads:51
22352235
--
22362236
Occurs: 2 times
22372237
<========================>
2238-
raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : failed precondition from range_check.ads:54
2238+
raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : failed precondition from range_check.ads:55
22392239

22402240
--
22412241
Occurs: 1 times

‎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:106|
1033+
| GNU Ada (ada2goto) Assert_Failure failed precondition from tree_walk.ads:109|
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:106|
1103+
| GNU Ada (ada2goto) Assert_Failure failed precondition from tree_walk.ads:109|
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:106|
1108+
| GNU Ada (ada2goto) Assert_Failure failed precondition from tree_walk.ads:109|
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:106|
1113+
| GNU Ada (ada2goto) Assert_Failure failed precondition from tree_walk.ads:109|
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
@@ -13,11 +13,6 @@ Calling function: Process_Declaration
1313
Error message: Use type clause declaration
1414
Nkind: N_Use_Type_Clause
1515
--
16-
Occurs: 18 times
17-
Calling function: Process_Pragma_Declaration
18-
Error message: Unsupported pragma: Suppress initialization
19-
Nkind: N_Pragma
20-
--
2116
Occurs: 2 times
2217
Calling function: Do_Expression
2318
Error message: ATTRIBUTE_ASM_OUTPUT unsupported
@@ -30,7 +25,7 @@ Raw compiler error message:
3025
--
3126
Occurs: 23 times
3227
+===========================GNAT BUG DETECTED==============================+
33-
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:54|
28+
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:55|
3429
Error detected at REDACTED
3530
--
3631
Occurs: 2 times
@@ -40,122 +35,122 @@ Error detected at REDACTED
4035
--
4136
Occurs: 1 times
4237
+===========================GNAT BUG DETECTED==============================+
43-
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:54|
38+
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:55|
4439
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

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

Lines changed: 0 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -78,11 +78,6 @@ Calling function: Do_Expression
7878
Error message: ATTRIBUTE_ASM_OUTPUT unsupported
7979
Nkind: N_Attribute_Reference
8080
--
81-
Occurs: 2 times
82-
Calling function: Process_Pragma_Declaration
83-
Error message: Known but unsupported pragma: Linker Options
84-
Nkind: N_Pragma
85-
--
8681
Occurs: 32 times
8782
Redacted compiler error message:
8883
file "REDACTED" not found

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2985,7 +2985,7 @@ Error detected at REDACTED
29852985
--
29862986
Occurs: 1 times
29872987
+===========================GNAT BUG DETECTED==============================+
2988-
| GNU Ada (ada2goto) Assert_Failure failed precondition from tree_walk.ads:106|
2988+
| GNU Ada (ada2goto) Assert_Failure failed precondition from tree_walk.ads:109|
29892989
Error detected at REDACTED
29902990
--
29912991
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: 3 times
2722
Calling function: Do_Expression
2823
Error message: ATTRIBUTE_IMAGE unsupported
@@ -305,5 +300,5 @@ Error detected at REDACTED
305300
--
306301
Occurs: 2 times
307302
<========================>
308-
raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : failed precondition from range_check.ads:54
303+
raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : failed precondition from range_check.ads:55
309304

0 commit comments

Comments
 (0)