Skip to content

Commit e5767e5

Browse files
tjj2017tjj2017
committed
Resolve conflicts and update golden results.
Merge branch 'nondet_model' of https://github.com/tjj2017/gnat2goto into nondet_model
2 parents 5ba7379 + 2c13a66 commit e5767e5

Some content is hidden

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

47 files changed

+1100
-176
lines changed

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

Lines changed: 17 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -13,11 +13,6 @@ 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: 163 times
2217
Calling function: Process_Pragma_Declaration
2318
Error message: pragma Export: Multi-language analysis unsupported
@@ -194,6 +189,11 @@ Error message: Unsupported pragma: Refine
194189
Nkind: N_Pragma
195190
--
196191
Occurs: 1 times
192+
Calling function: Process_Pragma_Declaration
193+
Error message: Unsupported pragma: Suppress initialization
194+
Nkind: N_Pragma
195+
--
196+
Occurs: 1 times
197197
Calling function: Process_Statement
198198
Error message: Unknown expression kind
199199
Nkind: N_Object_Renaming_Declaration
@@ -1770,12 +1770,12 @@ Error detected at REDACTED
17701770
--
17711771
Occurs: 1 times
17721772
+===========================GNAT BUG DETECTED==============================+
1773-
| GNU Ada (ada2goto) Assert_Failure failed precondition from arrays.ads:51 |
1773+
| GNU Ada (ada2goto) Assert_Failure failed precondition from arrays.ads:71 |
17741774
Error detected at REDACTED
17751775
--
17761776
Occurs: 1 times
17771777
+===========================GNAT BUG DETECTED==============================+
1778-
| GNU Ada (ada2goto) Assert_Failure failed precondition from arrays.ads:51 |
1778+
| GNU Ada (ada2goto) Assert_Failure failed precondition from arrays.ads:71 |
17791779
Error detected at REDACTED
17801780
--
17811781
Occurs: 1 times
@@ -2125,47 +2125,47 @@ Error detected at REDACTED
21252125
--
21262126
Occurs: 1 times
21272127
+===========================GNAT BUG DETECTED==============================+
2128-
| 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|
21292129
Error detected at REDACTED
21302130
--
21312131
Occurs: 1 times
21322132
+===========================GNAT BUG DETECTED==============================+
2133-
| 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|
21342134
Error detected at REDACTED
21352135
--
21362136
Occurs: 1 times
21372137
+===========================GNAT BUG DETECTED==============================+
2138-
| 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|
21392139
Error detected at REDACTED
21402140
--
21412141
Occurs: 1 times
21422142
+===========================GNAT BUG DETECTED==============================+
2143-
| 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|
21442144
Error detected at REDACTED
21452145
--
21462146
Occurs: 1 times
21472147
+===========================GNAT BUG DETECTED==============================+
2148-
| 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|
21492149
Error detected at REDACTED
21502150
--
21512151
Occurs: 1 times
21522152
+===========================GNAT BUG DETECTED==============================+
2153-
| 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|
21542154
Error detected at REDACTED
21552155
--
21562156
Occurs: 1 times
21572157
+===========================GNAT BUG DETECTED==============================+
2158-
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:54|
2158+
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:55|
21592159
Error detected at REDACTED
21602160
--
21612161
Occurs: 1 times
21622162
+===========================GNAT BUG DETECTED==============================+
2163-
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:54|
2163+
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:55|
21642164
Error detected at REDACTED
21652165
--
21662166
Occurs: 1 times
21672167
+===========================GNAT BUG DETECTED==============================+
2168-
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:54|
2168+
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:55|
21692169
Error detected at REDACTED
21702170
--
21712171
Occurs: 1 times
@@ -2245,12 +2245,7 @@ raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : failed precondition from arrays.ads:51
22452245
--
22462246
Occurs: 2 times
22472247
<========================>
2248-
raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : failed precondition from arrays.ads:57
2249-
2250-
--
2251-
Occurs: 2 times
2252-
<========================>
2253-
raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : failed precondition from range_check.ads:54
2248+
raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : failed precondition from range_check.ads:55
22542249

22552250
--
22562251
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: 1 times
72
Calling function: Process_Pragma_Declaration
83
Error message: pragma Import: Multi-language analysis unsupported

‎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: 9 times
2217
Calling function: Process_Pragma_Declaration
2318
Error message: pragma Import: Multi-language analysis 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
@@ -3180,7 +3180,7 @@ Error detected at REDACTED
31803180
--
31813181
Occurs: 1 times
31823182
+===========================GNAT BUG DETECTED==============================+
3183-
| GNU Ada (ada2goto) Assert_Failure failed precondition from tree_walk.ads:106|
3183+
| GNU Ada (ada2goto) Assert_Failure failed precondition from tree_walk.ads:109|
31843184
Error detected at REDACTED
31853185
--
31863186
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)