Skip to content

Commit 9a1badd

Browse files
committed
Update golden results.
Main differences are due to: Now reporting an unsupported node for multi-language imports/exports rather than a warning message. Pragma/aspect Global now acceptrd as a no-op for ASVAT analysis but meaningful for ASVAT modelling. In StratoX a failed precondition in arrays.ads seems to be replaced by an assertion failure in atree.adb. The precondition in arrays.ads is not changed by this mod, so the changes made to the code must now avoid this particular precondition failure but the code then fails later in atree.adb.
1 parent 6ec3ce7 commit 9a1badd

File tree

6 files changed

+43
-28
lines changed

6 files changed

+43
-28
lines changed

experiments/golden-results/StratoX-summary.txt

Lines changed: 23 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@ 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
@@ -18,6 +18,11 @@ Calling function: Process_Pragma_Declaration
1818
Error message: Unsupported pragma: Suppress initialization
1919
Nkind: N_Pragma
2020
--
21+
Occurs: 163 times
22+
Calling function: Process_Pragma_Declaration
23+
Error message: pragma Export: Multi-language analysis unsupported
24+
Nkind: N_Pragma
25+
--
2126
Occurs: 153 times
2227
Calling function: Process_Pragma_Declaration
2328
Error message: Unsupported pragma: Postcondition
@@ -38,11 +43,6 @@ Calling function: Do_Expression
3843
Error message: Index of string unsupported
3944
Nkind: N_Indexed_Component
4045
--
41-
Occurs: 14 times
42-
Calling function: Process_Pragma_Declaration
43-
Error message: Unsupported pragma: Global
44-
Nkind: N_Pragma
45-
--
4646
Occurs: 13 times
4747
Calling function: Do_Expression
4848
Error message: Last of string unsupported
@@ -113,6 +113,11 @@ Calling function: Do_Itype_Integer_Subtype
113113
Error message: Non-literal bound unsupported
114114
Nkind: N_Defining_Identifier
115115
--
116+
Occurs: 2 times
117+
Calling function: Process_Pragma_Declaration
118+
Error message: pragma Import: Multi-language analysis unsupported
119+
Nkind: N_Pragma
120+
--
116121
Occurs: 1 times
117122
Calling function: Do_Base_Range_Constraint
118123
Error message: unsupported lower range kind
@@ -1745,7 +1750,7 @@ Error detected at REDACTED
17451750
--
17461751
Occurs: 3 times
17471752
+===========================GNAT BUG DETECTED==============================+
1748-
| GNU Ada (ada2goto) Assert_Failure tree_walk.adb:992 |
1753+
| GNU Ada (ada2goto) Assert_Failure tree_walk.adb:989 |
17491754
Error detected at REDACTED
17501755
--
17511756
Occurs: 2 times
@@ -1760,6 +1765,11 @@ Error detected at REDACTED
17601765
--
17611766
Occurs: 1 times
17621767
+===========================GNAT BUG DETECTED==============================+
1768+
| GNU Ada (ada2goto) Assert_Failure atree.adb:992 |
1769+
Error detected at REDACTED
1770+
--
1771+
Occurs: 1 times
1772+
+===========================GNAT BUG DETECTED==============================+
17631773
| GNU Ada (ada2goto) Assert_Failure failed precondition from arrays.ads:51 |
17641774
Error detected at REDACTED
17651775
--
@@ -2160,7 +2170,7 @@ Error detected at REDACTED
21602170
--
21612171
Occurs: 1 times
21622172
+===========================GNAT BUG DETECTED==============================+
2163-
| GNU Ada (ada2goto) Assert_Failure failed precondition from tree_walk.adb:72|
2173+
| GNU Ada (ada2goto) Assert_Failure failed precondition from tree_walk.adb:73|
21642174
Error detected at REDACTED
21652175
--
21662176
Occurs: 1 times
@@ -2223,19 +2233,19 @@ Occurs: 25 times
22232233
raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : failed precondition from goto_utils.ads:147
22242234

22252235
--
2226-
Occurs: 4 times
2236+
Occurs: 2 times
22272237
<========================>
2228-
raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : failed precondition from arrays.ads:57
2238+
raised CONSTRAINT_ERROR : Symbol_Table_Info.Symbol_Maps.Constant_Reference: key not in map
22292239

22302240
--
22312241
Occurs: 2 times
22322242
<========================>
2233-
raised CONSTRAINT_ERROR : Symbol_Table_Info.Symbol_Maps.Constant_Reference: key not in map
2243+
raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : failed precondition from arrays.ads:51
22342244

22352245
--
22362246
Occurs: 2 times
22372247
<========================>
2238-
raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : failed precondition from arrays.ads:51
2248+
raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : failed precondition from arrays.ads:57
22392249

22402250
--
22412251
Occurs: 2 times
@@ -2245,5 +2255,5 @@ raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : failed precondition from range_check.a
22452255
--
22462256
Occurs: 1 times
22472257
<========================>
2248-
raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : failed precondition from tree_walk.adb:72
2258+
raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : failed precondition from tree_walk.adb:73
22492259

experiments/golden-results/UKNI-Information-Barrier-summary.txt

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,11 @@ Calling function: Do_Expression
1818
Error message: Last of string unsupported
1919
Nkind: N_Attribute_Reference
2020
--
21+
Occurs: 1 times
22+
Calling function: Process_Pragma_Declaration
23+
Error message: pragma Export: Multi-language analysis unsupported
24+
Nkind: N_Pragma
25+
--
2126
Occurs: 5 times
2227
Redacted compiler error message:
2328
"REDACTED" not declared in "REDACTED"

experiments/golden-results/ksum-summary.txt

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,11 @@ Calling function: Process_Pragma_Declaration
33
Error message: Unsupported pragma: Suppress initialization
44
Nkind: N_Pragma
55
--
6+
Occurs: 1 times
7+
Calling function: Process_Pragma_Declaration
8+
Error message: pragma Import: Multi-language analysis unsupported
9+
Nkind: N_Pragma
10+
--
611
Occurs: 41 times
712
Redacted compiler error message:
813
file "REDACTED" not found

experiments/golden-results/libkeccak-summary.txt

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,5 @@
11
Occurs: 423 times
22
Calling function: Process_Pragma_Declaration
3-
Error message: Unsupported pragma: Global
4-
Nkind: N_Pragma
5-
--
6-
Occurs: 423 times
7-
Calling function: Process_Pragma_Declaration
83
Error message: Unsupported pragma: Precondition
94
Nkind: N_Pragma
105
--
@@ -23,6 +18,11 @@ Calling function: Process_Pragma_Declaration
2318
Error message: Unsupported pragma: Suppress initialization
2419
Nkind: N_Pragma
2520
--
21+
Occurs: 9 times
22+
Calling function: Process_Pragma_Declaration
23+
Error message: pragma Import: Multi-language analysis unsupported
24+
Nkind: N_Pragma
25+
--
2626
Occurs: 2 times
2727
Calling function: Do_Expression
2828
Error message: ATTRIBUTE_ASM_OUTPUT unsupported

experiments/golden-results/libsparkcrypto-summary.txt

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -13,11 +13,6 @@ Calling function: Process_Pragma_Declaration
1313
Error message: Unsupported pragma: Postcondition
1414
Nkind: N_Pragma
1515
--
16-
Occurs: 105 times
17-
Calling function: Process_Pragma_Declaration
18-
Error message: Unsupported pragma: Global
19-
Nkind: N_Pragma
20-
--
2116
Occurs: 104 times
2217
Calling function: Process_Pragma_Declaration
2318
Error message: Unknown pragma: ghost
@@ -48,6 +43,11 @@ Calling function: Do_Itype_Integer_Subtype
4843
Error message: Non-literal bound unsupported
4944
Nkind: N_Defining_Identifier
5045
--
46+
Occurs: 26 times
47+
Calling function: Process_Pragma_Declaration
48+
Error message: pragma Import: Multi-language analysis unsupported
49+
Nkind: N_Pragma
50+
--
5151
Occurs: 24 times
5252
Calling function: Process_Declaration
5353
Error message: size clause not applied by the front-end

experiments/golden-results/muen-summary.txt

Lines changed: 0 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -30,11 +30,6 @@ Nkind: N_Pragma
3030
--
3131
Occurs: 8 times
3232
Calling function: Process_Pragma_Declaration
33-
Error message: Unsupported pragma: Global
34-
Nkind: N_Pragma
35-
--
36-
Occurs: 8 times
37-
Calling function: Process_Pragma_Declaration
3833
Error message: Unsupported pragma: Precondition
3934
Nkind: N_Pragma
4035
--

0 commit comments

Comments
 (0)