Skip to content

Commit 29737d1

Browse files
martin-csmartin-cs
authored
Merge branch 'master' into nondet_model
2 parents 5ba7379 + e81b928 commit 29737d1

File tree

24 files changed

+495
-88
lines changed

24 files changed

+495
-88
lines changed

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

Lines changed: 12 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -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
@@ -2250,7 +2250,7 @@ raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : failed precondition from arrays.ads:57
22502250
--
22512251
Occurs: 2 times
22522252
<========================>
2253-
raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : failed precondition from range_check.ads:54
2253+
raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : failed precondition from range_check.ads:55
22542254

22552255
--
22562256
Occurs: 1 times

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

Lines changed: 25 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -35,7 +35,7 @@ Raw compiler error message:
3535
--
3636
Occurs: 23 times
3737
+===========================GNAT BUG DETECTED==============================+
38-
| 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|
3939
Error detected at REDACTED
4040
--
4141
Occurs: 2 times
@@ -45,122 +45,122 @@ Error detected at REDACTED
4545
--
4646
Occurs: 1 times
4747
+===========================GNAT BUG DETECTED==============================+
48-
| 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|
4949
Error detected at REDACTED
5050
--
5151
Occurs: 1 times
5252
+===========================GNAT BUG DETECTED==============================+
53-
| 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|
5454
Error detected at REDACTED
5555
--
5656
Occurs: 1 times
5757
+===========================GNAT BUG DETECTED==============================+
58-
| 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|
5959
Error detected at REDACTED
6060
--
6161
Occurs: 1 times
6262
+===========================GNAT BUG DETECTED==============================+
63-
| 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|
6464
Error detected at REDACTED
6565
--
6666
Occurs: 1 times
6767
+===========================GNAT BUG DETECTED==============================+
68-
| 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|
6969
Error detected at REDACTED
7070
--
7171
Occurs: 1 times
7272
+===========================GNAT BUG DETECTED==============================+
73-
| 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|
7474
Error detected at REDACTED
7575
--
7676
Occurs: 1 times
7777
+===========================GNAT BUG DETECTED==============================+
78-
| 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|
7979
Error detected at REDACTED
8080
--
8181
Occurs: 1 times
8282
+===========================GNAT BUG DETECTED==============================+
83-
| 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|
8484
Error detected at REDACTED
8585
--
8686
Occurs: 1 times
8787
+===========================GNAT BUG DETECTED==============================+
88-
| 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|
8989
Error detected at REDACTED
9090
--
9191
Occurs: 1 times
9292
+===========================GNAT BUG DETECTED==============================+
93-
| 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|
9494
Error detected at REDACTED
9595
--
9696
Occurs: 1 times
9797
+===========================GNAT BUG DETECTED==============================+
98-
| 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|
9999
Error detected at REDACTED
100100
--
101101
Occurs: 1 times
102102
+===========================GNAT BUG DETECTED==============================+
103-
| 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|
104104
Error detected at REDACTED
105105
--
106106
Occurs: 1 times
107107
+===========================GNAT BUG DETECTED==============================+
108-
| 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|
109109
Error detected at REDACTED
110110
--
111111
Occurs: 1 times
112112
+===========================GNAT BUG DETECTED==============================+
113-
| 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|
114114
Error detected at REDACTED
115115
--
116116
Occurs: 1 times
117117
+===========================GNAT BUG DETECTED==============================+
118-
| 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|
119119
Error detected at REDACTED
120120
--
121121
Occurs: 1 times
122122
+===========================GNAT BUG DETECTED==============================+
123-
| 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|
124124
Error detected at REDACTED
125125
--
126126
Occurs: 1 times
127127
+===========================GNAT BUG DETECTED==============================+
128-
| 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|
129129
Error detected at REDACTED
130130
--
131131
Occurs: 1 times
132132
+===========================GNAT BUG DETECTED==============================+
133-
| 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|
134134
Error detected at REDACTED
135135
--
136136
Occurs: 1 times
137137
+===========================GNAT BUG DETECTED==============================+
138-
| 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|
139139
Error detected at REDACTED
140140
--
141141
Occurs: 1 times
142142
+===========================GNAT BUG DETECTED==============================+
143-
| 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|
144144
Error detected at REDACTED
145145
--
146146
Occurs: 1 times
147147
+===========================GNAT BUG DETECTED==============================+
148-
| 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|
149149
Error detected at REDACTED
150150
--
151151
Occurs: 1 times
152152
+===========================GNAT BUG DETECTED==============================+
153-
| 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|
154154
Error detected at REDACTED
155155
--
156156
Occurs: 1 times
157157
+===========================GNAT BUG DETECTED==============================+
158-
| 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|
159159
Error detected at REDACTED
160160
--
161161
Occurs: 1 times
162162
+===========================GNAT BUG DETECTED==============================+
163-
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:54|
163+
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:55|
164164
Error detected at REDACTED
165165
--
166166
Occurs: 1 times

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -310,5 +310,5 @@ Error detected at REDACTED
310310
--
311311
Occurs: 2 times
312312
<========================>
313-
raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : failed precondition from range_check.ads:54
313+
raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : failed precondition from range_check.ads:55
314314

0 commit comments

Comments
 (0)