Skip to content

Commit 2dac8ee

Browse files
martin-csmartin-cs
authored
Merge pull request #343 from tjj2017/iss_131_ready
Iss 131 ready
2 parents 645c41a + c4eb8be commit 2dac8ee

File tree

29 files changed

+2871
-299
lines changed

29 files changed

+2871
-299
lines changed

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

Lines changed: 90 additions & 95 deletions
Large diffs are not rendered by default.

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

Lines changed: 0 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -8,11 +8,6 @@ Calling function: Process_Pragma_Declaration
88
Error message: Unsupported pragma: Precondition
99
Nkind: N_Pragma
1010
--
11-
Occurs: 190 times
12-
Calling function: Process_Declaration
13-
Error message: size clause not applied by the front-end
14-
Nkind: N_Attribute_Definition_Clause
15-
--
1611
Occurs: 47 times
1712
Calling function: Process_Declaration
1813
Error message: Use type clause declaration

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

Lines changed: 0 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -48,11 +48,6 @@ Calling function: Do_Itype_Integer_Subtype
4848
Error message: Non-literal bound unsupported
4949
Nkind: N_Defining_Identifier
5050
--
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-
--
5651
Occurs: 23 times
5752
Calling function: Do_Expression
5853
Error message: Quantified

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

Lines changed: 44 additions & 49 deletions
Original file line numberDiff line numberDiff line change
@@ -3,11 +3,6 @@ Calling function: Process_Declaration
33
Error message: Use type clause declaration
44
Nkind: N_Use_Type_Clause
55
--
6-
Occurs: 56 times
7-
Calling function: Process_Declaration
8-
Error message: size clause not applied by the front-end
9-
Nkind: N_Attribute_Definition_Clause
10-
--
116
Occurs: 13 times
127
Calling function: Do_Derived_Type_Definition
138
Error message: record extension unsupported
@@ -2970,222 +2965,222 @@ Error detected at REDACTED
29702965
--
29712966
Occurs: 2 times
29722967
+===========================GNAT BUG DETECTED==============================+
2973-
| GNU Ada (ada2goto) Assert_Failure failed precondition from ireps.ads:1784|
2968+
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:2534 |
29742969
Error detected at REDACTED
29752970
--
29762971
Occurs: 2 times
29772972
+===========================GNAT BUG DETECTED==============================+
2978-
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:2534 |
2973+
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 |
29792974
Error detected at REDACTED
29802975
--
29812976
Occurs: 1 times
29822977
+===========================GNAT BUG DETECTED==============================+
2983-
| GNU Ada (ada2goto) Assert_Failure failed precondition from ireps.ads:1784|
2978+
| GNU Ada (ada2goto) Assert_Failure failed precondition from tree_walk.ads:108|
29842979
Error detected at REDACTED
29852980
--
29862981
Occurs: 1 times
29872982
+===========================GNAT BUG DETECTED==============================+
2988-
| GNU Ada (ada2goto) Assert_Failure failed precondition from ireps.ads:1784|
2983+
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:2534 |
29892984
Error detected at REDACTED
29902985
--
29912986
Occurs: 1 times
29922987
+===========================GNAT BUG DETECTED==============================+
2993-
| GNU Ada (ada2goto) Assert_Failure failed precondition from ireps.ads:1784|
2988+
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:2534 |
29942989
Error detected at REDACTED
29952990
--
29962991
Occurs: 1 times
29972992
+===========================GNAT BUG DETECTED==============================+
2998-
| GNU Ada (ada2goto) Assert_Failure failed precondition from ireps.ads:1784|
2993+
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 |
29992994
Error detected at REDACTED
30002995
--
30012996
Occurs: 1 times
30022997
+===========================GNAT BUG DETECTED==============================+
3003-
| GNU Ada (ada2goto) Assert_Failure failed precondition from ireps.ads:1784|
2998+
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 |
30042999
Error detected at REDACTED
30053000
--
30063001
Occurs: 1 times
30073002
+===========================GNAT BUG DETECTED==============================+
3008-
| GNU Ada (ada2goto) Assert_Failure failed precondition from ireps.ads:1784|
3003+
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 |
30093004
Error detected at REDACTED
30103005
--
30113006
Occurs: 1 times
30123007
+===========================GNAT BUG DETECTED==============================+
3013-
| GNU Ada (ada2goto) Assert_Failure failed precondition from ireps.ads:1784|
3008+
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 |
30143009
Error detected at REDACTED
30153010
--
30163011
Occurs: 1 times
30173012
+===========================GNAT BUG DETECTED==============================+
3018-
| GNU Ada (ada2goto) Assert_Failure failed precondition from ireps.ads:1784|
3013+
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 |
30193014
Error detected at REDACTED
30203015
--
30213016
Occurs: 1 times
30223017
+===========================GNAT BUG DETECTED==============================+
3023-
| GNU Ada (ada2goto) Assert_Failure failed precondition from ireps.ads:1784|
3018+
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 |
30243019
Error detected at REDACTED
30253020
--
30263021
Occurs: 1 times
30273022
+===========================GNAT BUG DETECTED==============================+
3028-
| GNU Ada (ada2goto) Assert_Failure failed precondition from ireps.ads:1784|
3023+
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 |
30293024
Error detected at REDACTED
30303025
--
30313026
Occurs: 1 times
30323027
+===========================GNAT BUG DETECTED==============================+
3033-
| GNU Ada (ada2goto) Assert_Failure failed precondition from ireps.ads:1784|
3028+
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 |
30343029
Error detected at REDACTED
30353030
--
30363031
Occurs: 1 times
30373032
+===========================GNAT BUG DETECTED==============================+
3038-
| GNU Ada (ada2goto) Assert_Failure failed precondition from ireps.ads:1784|
3033+
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 |
30393034
Error detected at REDACTED
30403035
--
30413036
Occurs: 1 times
30423037
+===========================GNAT BUG DETECTED==============================+
3043-
| GNU Ada (ada2goto) Assert_Failure failed precondition from ireps.ads:1784|
3038+
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 |
30443039
Error detected at REDACTED
30453040
--
30463041
Occurs: 1 times
30473042
+===========================GNAT BUG DETECTED==============================+
3048-
| GNU Ada (ada2goto) Assert_Failure failed precondition from ireps.ads:1784|
3043+
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 |
30493044
Error detected at REDACTED
30503045
--
30513046
Occurs: 1 times
30523047
+===========================GNAT BUG DETECTED==============================+
3053-
| GNU Ada (ada2goto) Assert_Failure failed precondition from ireps.ads:1784|
3048+
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 |
30543049
Error detected at REDACTED
30553050
--
30563051
Occurs: 1 times
30573052
+===========================GNAT BUG DETECTED==============================+
3058-
| GNU Ada (ada2goto) Assert_Failure failed precondition from ireps.ads:1784|
3053+
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 |
30593054
Error detected at REDACTED
30603055
--
30613056
Occurs: 1 times
30623057
+===========================GNAT BUG DETECTED==============================+
3063-
| GNU Ada (ada2goto) Assert_Failure failed precondition from ireps.ads:1784|
3058+
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 |
30643059
Error detected at REDACTED
30653060
--
30663061
Occurs: 1 times
30673062
+===========================GNAT BUG DETECTED==============================+
3068-
| GNU Ada (ada2goto) Assert_Failure failed precondition from ireps.ads:1784|
3063+
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 |
30693064
Error detected at REDACTED
30703065
--
30713066
Occurs: 1 times
30723067
+===========================GNAT BUG DETECTED==============================+
3073-
| GNU Ada (ada2goto) Assert_Failure failed precondition from ireps.ads:1784|
3068+
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 |
30743069
Error detected at REDACTED
30753070
--
30763071
Occurs: 1 times
30773072
+===========================GNAT BUG DETECTED==============================+
3078-
| GNU Ada (ada2goto) Assert_Failure failed precondition from ireps.ads:1784|
3073+
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 |
30793074
Error detected at REDACTED
30803075
--
30813076
Occurs: 1 times
30823077
+===========================GNAT BUG DETECTED==============================+
3083-
| GNU Ada (ada2goto) Assert_Failure failed precondition from ireps.ads:1784|
3078+
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 |
30843079
Error detected at REDACTED
30853080
--
30863081
Occurs: 1 times
30873082
+===========================GNAT BUG DETECTED==============================+
3088-
| GNU Ada (ada2goto) Assert_Failure failed precondition from ireps.ads:1784|
3083+
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 |
30893084
Error detected at REDACTED
30903085
--
30913086
Occurs: 1 times
30923087
+===========================GNAT BUG DETECTED==============================+
3093-
| GNU Ada (ada2goto) Assert_Failure failed precondition from ireps.ads:1784|
3088+
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 |
30943089
Error detected at REDACTED
30953090
--
30963091
Occurs: 1 times
30973092
+===========================GNAT BUG DETECTED==============================+
3098-
| GNU Ada (ada2goto) Assert_Failure failed precondition from ireps.ads:1784|
3093+
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 |
30993094
Error detected at REDACTED
31003095
--
31013096
Occurs: 1 times
31023097
+===========================GNAT BUG DETECTED==============================+
3103-
| GNU Ada (ada2goto) Assert_Failure failed precondition from ireps.ads:1784|
3098+
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 |
31043099
Error detected at REDACTED
31053100
--
31063101
Occurs: 1 times
31073102
+===========================GNAT BUG DETECTED==============================+
3108-
| GNU Ada (ada2goto) Assert_Failure failed precondition from ireps.ads:1784|
3103+
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 |
31093104
Error detected at REDACTED
31103105
--
31113106
Occurs: 1 times
31123107
+===========================GNAT BUG DETECTED==============================+
3113-
| GNU Ada (ada2goto) Assert_Failure failed precondition from ireps.ads:1784|
3108+
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 |
31143109
Error detected at REDACTED
31153110
--
31163111
Occurs: 1 times
31173112
+===========================GNAT BUG DETECTED==============================+
3118-
| GNU Ada (ada2goto) Assert_Failure failed precondition from ireps.ads:1784|
3113+
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 |
31193114
Error detected at REDACTED
31203115
--
31213116
Occurs: 1 times
31223117
+===========================GNAT BUG DETECTED==============================+
3123-
| GNU Ada (ada2goto) Assert_Failure failed precondition from ireps.ads:1784|
3118+
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 |
31243119
Error detected at REDACTED
31253120
--
31263121
Occurs: 1 times
31273122
+===========================GNAT BUG DETECTED==============================+
3128-
| GNU Ada (ada2goto) Assert_Failure failed precondition from ireps.ads:1784|
3123+
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 |
31293124
Error detected at REDACTED
31303125
--
31313126
Occurs: 1 times
31323127
+===========================GNAT BUG DETECTED==============================+
3133-
| GNU Ada (ada2goto) Assert_Failure failed precondition from ireps.ads:1784|
3128+
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 |
31343129
Error detected at REDACTED
31353130
--
31363131
Occurs: 1 times
31373132
+===========================GNAT BUG DETECTED==============================+
3138-
| GNU Ada (ada2goto) Assert_Failure failed precondition from ireps.ads:1784|
3133+
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 |
31393134
Error detected at REDACTED
31403135
--
31413136
Occurs: 1 times
31423137
+===========================GNAT BUG DETECTED==============================+
3143-
| GNU Ada (ada2goto) Assert_Failure failed precondition from ireps.ads:1784|
3138+
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 |
31443139
Error detected at REDACTED
31453140
--
31463141
Occurs: 1 times
31473142
+===========================GNAT BUG DETECTED==============================+
3148-
| GNU Ada (ada2goto) Assert_Failure failed precondition from ireps.ads:1784|
3143+
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 |
31493144
Error detected at REDACTED
31503145
--
31513146
Occurs: 1 times
31523147
+===========================GNAT BUG DETECTED==============================+
3153-
| GNU Ada (ada2goto) Assert_Failure failed precondition from ireps.ads:1784|
3148+
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 |
31543149
Error detected at REDACTED
31553150
--
31563151
Occurs: 1 times
31573152
+===========================GNAT BUG DETECTED==============================+
3158-
| GNU Ada (ada2goto) Assert_Failure failed precondition from ireps.ads:1784|
3153+
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 |
31593154
Error detected at REDACTED
31603155
--
31613156
Occurs: 1 times
31623157
+===========================GNAT BUG DETECTED==============================+
3163-
| GNU Ada (ada2goto) Assert_Failure failed precondition from ireps.ads:1784|
3158+
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 |
31643159
Error detected at REDACTED
31653160
--
31663161
Occurs: 1 times
31673162
+===========================GNAT BUG DETECTED==============================+
3168-
| GNU Ada (ada2goto) Assert_Failure failed precondition from ireps.ads:1784|
3163+
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 |
31693164
Error detected at REDACTED
31703165
--
31713166
Occurs: 1 times
31723167
+===========================GNAT BUG DETECTED==============================+
3173-
| GNU Ada (ada2goto) Assert_Failure failed precondition from ireps.ads:1784|
3168+
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 |
31743169
Error detected at REDACTED
31753170
--
31763171
Occurs: 1 times
31773172
+===========================GNAT BUG DETECTED==============================+
3178-
| GNU Ada (ada2goto) Assert_Failure failed precondition from tree_walk.ads:108|
3173+
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 |
31793174
Error detected at REDACTED
31803175
--
31813176
Occurs: 1 times
31823177
+===========================GNAT BUG DETECTED==============================+
3183-
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:2534 |
3178+
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 |
31843179
Error detected at REDACTED
31853180
--
31863181
Occurs: 1 times
31873182
+===========================GNAT BUG DETECTED==============================+
3188-
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:2534 |
3183+
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 |
31893184
Error detected at REDACTED
31903185
--
31913186
Occurs: 1 times

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

Lines changed: 2 additions & 7 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: 4 times
22-
Calling function: Process_Declaration
23-
Error message: size clause not applied by the front-end
24-
Nkind: N_Attribute_Definition_Clause
25-
--
2621
Occurs: 3 times
2722
Calling function: Do_Expression
2823
Error message: ATTRIBUTE_IMAGE unsupported
@@ -110,12 +105,12 @@ Raw compiler error message:
110105
--
111106
Occurs: 1 times
112107
+===========================GNAT BUG DETECTED==============================+
113-
| GNU Ada (ada2goto) Assert_Failure failed precondition from ireps.ads:1784|
108+
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 |
114109
Error detected at REDACTED
115110
--
116111
Occurs: 1 times
117112
+===========================GNAT BUG DETECTED==============================+
118-
| GNU Ada (ada2goto) Assert_Failure failed precondition from ireps.ads:1784|
113+
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 |
119114
Error detected at REDACTED
120115
--
121116
Occurs: 1 times

0 commit comments

Comments
 (0)