Skip to content

Commit 2c4dcab

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 4fbe906 commit 2c4dcab

File tree

6 files changed

+36
-21
lines changed

6 files changed

+36
-21
lines changed

experiments/golden-results/StratoX-summary.txt

Lines changed: 11 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,11 @@ Calling function: Process_Declaration
88
Error message: Unknown declaration kind
99
Nkind: N_Validate_Unchecked_Conversion
1010
--
11+
Occurs: 163 times
12+
Calling function: Process_Pragma_Declaration
13+
Error message: pragma Export: Multi-language analysis unsupported
14+
Nkind: N_Pragma
15+
--
1116
Occurs: 152 times
1217
Calling function: Process_Pragma_Declaration
1318
Error message: Unsupported pragma: Postcondition
@@ -33,11 +38,6 @@ Calling function: Do_Expression
3338
Error message: Last of string unsupported
3439
Nkind: N_Attribute_Reference
3540
--
36-
Occurs: 13 times
37-
Calling function: Process_Pragma_Declaration
38-
Error message: Unsupported pragma: Global
39-
Nkind: N_Pragma
40-
--
4141
Occurs: 10 times
4242
Calling function: Do_Expression
4343
Error message: ATTRIBUTE_MACHINE unsupported
@@ -103,6 +103,11 @@ Calling function: Do_Itype_Integer_Subtype
103103
Error message: Non-literal bound unsupported
104104
Nkind: N_Defining_Identifier
105105
--
106+
Occurs: 2 times
107+
Calling function: Process_Pragma_Declaration
108+
Error message: pragma Import: Multi-language analysis unsupported
109+
Nkind: N_Pragma
110+
--
106111
Occurs: 1 times
107112
Calling function: Do_Base_Range_Constraint
108113
Error message: unsupported lower range kind
@@ -2150,7 +2155,7 @@ Error detected at REDACTED
21502155
--
21512156
Occurs: 1 times
21522157
+===========================GNAT BUG DETECTED==============================+
2153-
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 |
2158+
| GNU Ada (ada2goto) Assert_Failure failed precondition from tree_walk.adb:73|
21542159
Error detected at REDACTED
21552160
--
21562161
Occurs: 1 times

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
@@ -1,3 +1,8 @@
1+
Occurs: 1 times
2+
Calling function: Process_Pragma_Declaration
3+
Error message: pragma Import: Multi-language analysis unsupported
4+
Nkind: N_Pragma
5+
--
16
Occurs: 41 times
27
Redacted compiler error message:
38
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
--
@@ -13,6 +8,11 @@ Calling function: Process_Declaration
138
Error message: Use type clause declaration
149
Nkind: N_Use_Type_Clause
1510
--
11+
Occurs: 9 times
12+
Calling function: Process_Pragma_Declaration
13+
Error message: pragma Import: Multi-language analysis unsupported
14+
Nkind: N_Pragma
15+
--
1616
Occurs: 2 times
1717
Calling function: Do_Expression
1818
Error message: ATTRIBUTE_ASM_OUTPUT unsupported

experiments/golden-results/libsparkcrypto-summary.txt

Lines changed: 10 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,16 @@ 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+
--
51+
Occurs: 24 times
52+
Calling function: Process_Declaration
53+
Error message: size clause not applied by the front-end
54+
Nkind: N_Attribute_Definition_Clause
55+
--
5156
Occurs: 23 times
5257
Calling function: Do_Expression
5358
Error message: Quantified

experiments/golden-results/muen-summary.txt

Lines changed: 0 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -25,11 +25,6 @@ Nkind: N_Pragma
2525
--
2626
Occurs: 8 times
2727
Calling function: Process_Pragma_Declaration
28-
Error message: Unsupported pragma: Global
29-
Nkind: N_Pragma
30-
--
31-
Occurs: 8 times
32-
Calling function: Process_Pragma_Declaration
3328
Error message: Unsupported pragma: Precondition
3429
Nkind: N_Pragma
3530
--

0 commit comments

Comments
 (0)