Skip to content

Commit e81b928

Browse files
martin-csmartin-cs
authored
Merge pull request #345 from tjj2017/missing_from_precondition
Missing from precondition
2 parents 6247ed3 + d698a50 commit e81b928

File tree

4 files changed

+39
-38
lines changed

4 files changed

+39
-38
lines changed

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

Lines changed: 10 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -2115,47 +2115,47 @@ Error detected at REDACTED
21152115
--
21162116
Occurs: 1 times
21172117
+===========================GNAT BUG DETECTED==============================+
2118-
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:54|
2118+
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:55|
21192119
Error detected at REDACTED
21202120
--
21212121
Occurs: 1 times
21222122
+===========================GNAT BUG DETECTED==============================+
2123-
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:54|
2123+
| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:55|
21242124
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
@@ -2240,7 +2240,7 @@ raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : failed precondition from ireps.ads:164
22402240
--
22412241
Occurs: 2 times
22422242
<========================>
2243-
raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : failed precondition from range_check.ads:54
2243+
raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : failed precondition from range_check.ads:55
22442244

22452245
--
22462246
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

‎gnat2goto/driver/range_check.ads

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -24,15 +24,16 @@ package Range_Check is
2424
with Pre => Kind (Bound_Type) in
2525
I_Bounded_Unsignedbv_Type | I_Bounded_Signedbv_Type
2626
| I_Bounded_Floatbv_Type | I_Unsignedbv_Type | I_Signedbv_Type
27-
| I_Floatbv_Type,
27+
| I_Floatbv_Type | I_C_Enum_Type,
2828
Post => Kind (Get_Bound'Result) in Class_Expr;
2929

3030
function Get_Bound_Of_Bounded_Type (Bound_Type : Irep;
3131
Pos : Bound_Low_Or_High) return Irep
3232
with Pre => Kind (Bound_Type) in
3333
I_Bounded_Signedbv_Type
3434
| I_Bounded_Floatbv_Type
35-
| I_Bounded_Unsignedbv_Type,
35+
| I_Bounded_Unsignedbv_Type
36+
| I_C_Enum_Type,
3637
Post => Kind (Get_Bound_Of_Bounded_Type'Result) in Class_Expr;
3738

3839
function Make_Div_Zero_Assert_Expr (N : Node_Id; Value : Irep;

0 commit comments

Comments
 (0)