diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 75665dec0631f0844c434e7dacb8be41d85acee8..13bf2fc6abd65e107e330649546837b6276740f5 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -8548,6 +8548,9 @@ and doInit local_env asconst add_implicit_ensures preinit so acc initl =
if first < 0 || first > last then
Kernel.error ~once:true ~current:true
"start index larger than end index in range initializer";
+ (* Arbitrary limit to avoid building an impractical AST. *)
+ if last - first > 100_000 then
+ Kernel.fatal ~current:true "INDEX_RANGE too large";
let rec loop (i: int) =
if i > last then restil
else
@@ -10103,6 +10106,8 @@ and doStatement local_env (s : Cabs.statement) : chunk =
"Cannot understand the constants in case range"
in
if il > ih then Kernel.error ~once:true ~current:true "Empty case range";
+ (* Arbitrary limit to avoid building an impractical AST. *)
+ if ih - il > 100_000 then Kernel.fatal ~current:true "Case range too large";
let rec mkAll (i: int) =
if i > ih then [] else integer ~loc i :: mkAll (i + 1)
in
diff --git a/src/plugins/value/partitioning/partitioning_parameters.ml b/src/plugins/value/partitioning/partitioning_parameters.ml
index 1c8dae31e042b527e8e036cf404045966d193176..4ddcf1835217ca9caa6cdfdd8bd8c3f28c1979ce 100644
--- a/src/plugins/value/partitioning/partitioning_parameters.ml
+++ b/src/plugins/value/partitioning/partitioning_parameters.ml
@@ -93,15 +93,13 @@ struct
let t =
Cil.visitCilTerm (new Logic_utils.simplify_const_lval global_init) t
in
- let i = Logic_utils.constFoldTermToInt t in
- match Option.bind i Integer.to_int_opt with
- | Some n -> Partition.IntLimit n
- | None ->
- try Partition.ExpLimit (term_to_exp t)
- with Db.Properties.Interp.No_conversion ->
- warn "loop unrolling parameters must be valid expressions; \
- ignoring";
- default
+ try
+ match Logic_utils.constFoldTermToInt t with
+ | Some n -> Partition.IntLimit (Integer.to_int_exn n)
+ | None -> Partition.ExpLimit (term_to_exp t)
+ with Z.Overflow | Db.Properties.Interp.No_conversion ->
+ warn "invalid loop unrolling parameter; ignoring";
+ default
end
| _ ->
warn "invalid unroll annotation; ignoring";
diff --git a/tests/syntax/oracle/very_large_integers.0.res.oracle b/tests/syntax/oracle/very_large_integers.0.res.oracle
index db573af932d7288a94e547a1e729ad2581a7c585..82d87fd91ea4e7857cd258c3f5d04c06add50868 100644
--- a/tests/syntax/oracle/very_large_integers.0.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.0.res.oracle
@@ -1,11 +1,11 @@
[kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
-[kernel] tests/syntax/very_large_integers.c:22: User Error:
- integer constant too large in expression (unsigned long long)999999999999999999 + 9999999999999999999
[kernel] tests/syntax/very_large_integers.c:23: User Error:
+ integer constant too large in expression (unsigned long long)999999999999999999 + 9999999999999999999
+[kernel] tests/syntax/very_large_integers.c:24: User Error:
bitfield width is not a valid integer constant
-[kernel] tests/syntax/very_large_integers.c:58: Warning:
+[kernel] tests/syntax/very_large_integers.c:72: Warning:
ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] tests/syntax/very_large_integers.c:58: Warning:
+[kernel] tests/syntax/very_large_integers.c:72: Warning:
ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
(9223372036854775808) )
[kernel] User Error: stopping on file "tests/syntax/very_large_integers.c" that has errors. Add
diff --git a/tests/syntax/oracle/very_large_integers.1.res.oracle b/tests/syntax/oracle/very_large_integers.1.res.oracle
index 23cfa866c0b1679b16c8da7e786139aeb6c49151..36520f72626179395d229bbc84a9b7eaf13b0cfb 100644
--- a/tests/syntax/oracle/very_large_integers.1.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.1.res.oracle
@@ -1,11 +1,11 @@
[kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
-[kernel] tests/syntax/very_large_integers.c:29: User Error:
+[kernel] tests/syntax/very_large_integers.c:30: User Error:
Cannot represent the integer 99999999999999999999U
-[kernel] tests/syntax/very_large_integers.c:29: User Error:
+[kernel] tests/syntax/very_large_integers.c:30: User Error:
Cannot represent the integer 99999999999999999999U
-[kernel] tests/syntax/very_large_integers.c:58: Warning:
+[kernel] tests/syntax/very_large_integers.c:72: Warning:
ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] tests/syntax/very_large_integers.c:58: Warning:
+[kernel] tests/syntax/very_large_integers.c:72: Warning:
ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
(9223372036854775808) )
[kernel] User Error: stopping on file "tests/syntax/very_large_integers.c" that has errors. Add
diff --git a/tests/syntax/oracle/very_large_integers.10.res.oracle b/tests/syntax/oracle/very_large_integers.10.res.oracle
index 4f848474e09b65819663cd76d18d5f514f53c968..bf0d3aae1c5fa5982ac87923e34ab8598b9009d9 100644
--- a/tests/syntax/oracle/very_large_integers.10.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.10.res.oracle
@@ -1,11 +1,11 @@
[kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
-[kernel] tests/syntax/very_large_integers.c:58: Warning:
+[kernel] tests/syntax/very_large_integers.c:72: Warning:
ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] tests/syntax/very_large_integers.c:58: Warning:
+[kernel] tests/syntax/very_large_integers.c:72: Warning:
ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
(9223372036854775808) )
-[kernel] tests/syntax/very_large_integers.c:84: User Error:
- Invalid digit 9 in integer literal '09' in base 8.
+[kernel] tests/syntax/very_large_integers.c:85: Failure:
+ Invalid digit 9 in integer literal '09876543210' in base 8.
[kernel] User Error: stopping on file "tests/syntax/very_large_integers.c" that has errors. Add
'-kernel-msg-key pp' for preprocessing command.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/very_large_integers.11.res.oracle b/tests/syntax/oracle/very_large_integers.11.res.oracle
index c352a476c8d0b1515924c1ac46c2014c9c8c1d55..d11b5f4ef8b45e29969ac2f1aed40ed8bcf05682 100644
--- a/tests/syntax/oracle/very_large_integers.11.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.11.res.oracle
@@ -1,22 +1,36 @@
[kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
-[kernel] tests/syntax/very_large_integers.c:58: Warning:
+[kernel] tests/syntax/very_large_integers.c:72: Warning:
ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] tests/syntax/very_large_integers.c:58: Warning:
+[kernel] tests/syntax/very_large_integers.c:72: Warning:
ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
(9223372036854775808) )
-[kernel] tests/syntax/very_large_integers.c:89: Warning:
- ignoring unrolling directive (not an understood constant expression)
-/* Generated by Frama-C */
-int volatile nondet;
-/*@ logic ℤ too_large_integer= 9999999999999999999;
- */
-int main(void)
-{
- int __retres;
- /*@ loop pragma UNROLL 99999999999999999999; */
- while (nondet) ;
- __retres = 0;
- return __retres;
-}
-
-
+[kernel:annot-error] tests/syntax/very_large_integers.c:94: Warning:
+ Invalid slevel directive. Ignoring code annotation
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+ nondet ∈ [--..--]
+[kernel:annot-error] tests/syntax/very_large_integers.c:91: Warning:
+ invalid loop unrolling parameter; ignoring
+[kernel:annot-error] tests/syntax/very_large_integers.c:93: Warning:
+ invalid loop unrolling parameter; ignoring
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main:
+ __retres ∈ {0}
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 1 function analyzed (out of 1): 100% coverage.
+ In this function, 14 statements reached (out of 14): 100% coverage.
+ ----------------------------------------------------------------------------
+ Some errors and warnings have been raised during the analysis:
+ by the Eva analyzer: 0 errors 0 warnings
+ by the Frama-C kernel: 0 errors 5 warnings
+ ----------------------------------------------------------------------------
+ 0 alarms generated by the analysis.
+ ----------------------------------------------------------------------------
+ No logical properties have been reached by the analysis.
+ ----------------------------------------------------------------------------
+[kernel] Warning: warning annot-error treated as deferred error. See above messages for more information.
+[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/very_large_integers.12.res.oracle b/tests/syntax/oracle/very_large_integers.12.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..ae1f62ddcbb1abe403c9f5487710adca67bb18d0
--- /dev/null
+++ b/tests/syntax/oracle/very_large_integers.12.res.oracle
@@ -0,0 +1,11 @@
+[kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
+[kernel] tests/syntax/very_large_integers.c:72: Warning:
+ ignoring invalid aligned attribute: __aligned__(9223372036854775808)
+[kernel] tests/syntax/very_large_integers.c:72: Warning:
+ ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
+ (9223372036854775808) )
+[kernel] tests/syntax/very_large_integers.c:98: User Error:
+ Invalid digit 9 in integer literal '09' in base 8.
+[kernel] User Error: stopping on file "tests/syntax/very_large_integers.c" that has errors. Add
+ '-kernel-msg-key pp' for preprocessing command.
+[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/very_large_integers.13.res.oracle b/tests/syntax/oracle/very_large_integers.13.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..a415c2454fb8c4b6e6f50ce642a37f848e824d73
--- /dev/null
+++ b/tests/syntax/oracle/very_large_integers.13.res.oracle
@@ -0,0 +1,22 @@
+[kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
+[kernel] tests/syntax/very_large_integers.c:72: Warning:
+ ignoring invalid aligned attribute: __aligned__(9223372036854775808)
+[kernel] tests/syntax/very_large_integers.c:72: Warning:
+ ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
+ (9223372036854775808) )
+[kernel] tests/syntax/very_large_integers.c:103: Warning:
+ ignoring unrolling directive (not an understood constant expression)
+/* Generated by Frama-C */
+int volatile nondet;
+/*@ logic ℤ too_large_integer= 9999999999999999999;
+ */
+int main(void)
+{
+ int __retres;
+ /*@ loop pragma UNROLL 99999999999999999999; */
+ while (nondet) ;
+ __retres = 0;
+ return __retres;
+}
+
+
diff --git a/tests/syntax/oracle/very_large_integers.2.res.oracle b/tests/syntax/oracle/very_large_integers.2.res.oracle
index bb5f47fe756242bc9ba320bc6435621eb289b4e1..25740fed33da86b20117393d4a25f8919e975238 100644
--- a/tests/syntax/oracle/very_large_integers.2.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.2.res.oracle
@@ -1,7 +1,7 @@
[kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
-[kernel] tests/syntax/very_large_integers.c:36: User Error:
+[kernel] tests/syntax/very_large_integers.c:37: User Error:
integer constant too large in expression 9999999999999999999U
-[kernel] tests/syntax/very_large_integers.c:36: Failure:
+[kernel] tests/syntax/very_large_integers.c:37: Failure:
Cannot understand the constants in case range
[kernel] User Error: stopping on file "tests/syntax/very_large_integers.c" that has errors. Add
'-kernel-msg-key pp' for preprocessing command.
diff --git a/tests/syntax/oracle/very_large_integers.3.res.oracle b/tests/syntax/oracle/very_large_integers.3.res.oracle
index ad9de534b05aef91ec8a722ad0b193c72ef89375..f4cbe4f4e6d14e2acf9f68cbbcc46c39d8f90a12 100644
--- a/tests/syntax/oracle/very_large_integers.3.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.3.res.oracle
@@ -1,6 +1,5 @@
[kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
-[kernel] tests/syntax/very_large_integers.c:41: Failure:
- Array length 9999999999999999999U is not a compile-time constant: no explicit initializer allowed.
+[kernel] tests/syntax/very_large_integers.c:45: Failure: Case range too large
[kernel] User Error: stopping on file "tests/syntax/very_large_integers.c" that has errors. Add
'-kernel-msg-key pp' for preprocessing command.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/very_large_integers.4.res.oracle b/tests/syntax/oracle/very_large_integers.4.res.oracle
index 0d8599e32958e49f9a178eaa551bc2692388d0cb..e53651c2f5bff8cd11135c4216465253a4faf8c0 100644
--- a/tests/syntax/oracle/very_large_integers.4.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.4.res.oracle
@@ -1,12 +1,6 @@
[kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
-[kernel] tests/syntax/very_large_integers.c:45: User Error:
- INDEX initialization designator overflows
- 43
- 44 #ifdef INIT_DESIGNATOR2
- 45 int arr3[1] = { [9999999999999999999U] = 42 };
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- 46 #endif
- 47
+[kernel] tests/syntax/very_large_integers.c:50: Failure:
+ Array length 9999999999999999999U is not a compile-time constant: no explicit initializer allowed.
[kernel] User Error: stopping on file "tests/syntax/very_large_integers.c" that has errors. Add
'-kernel-msg-key pp' for preprocessing command.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/very_large_integers.5.res.oracle b/tests/syntax/oracle/very_large_integers.5.res.oracle
index 1798bfe46e3610238348f88b53f77a757bb82440..028afa06f27e1524caf054410fd66a022790e970 100644
--- a/tests/syntax/oracle/very_large_integers.5.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.5.res.oracle
@@ -1,10 +1,12 @@
[kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
-[kernel] tests/syntax/very_large_integers.c:49: User Error:
- integer constant too large in expression -9999999999999999999U
-[kernel] tests/syntax/very_large_integers.c:49: User Error:
- integer constant too large in expression 9999999999999999999U
-[kernel] tests/syntax/very_large_integers.c:49: Failure:
- INDEX_RANGE initialization designator is not a valid constant
+[kernel] tests/syntax/very_large_integers.c:54: User Error:
+ INDEX initialization designator overflows
+ 52
+ 53 #ifdef INIT_DESIGNATOR2
+ 54 int arr3[1] = { [9999999999999999999U] = 42 };
+ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ 55 #endif
+ 56
[kernel] User Error: stopping on file "tests/syntax/very_large_integers.c" that has errors. Add
'-kernel-msg-key pp' for preprocessing command.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/very_large_integers.6.res.oracle b/tests/syntax/oracle/very_large_integers.6.res.oracle
index c531dfb15a1f18822fb312d21c18796860aae437..80ea4f9cf539e9e3643304efad8bd4760c7ffb06 100644
--- a/tests/syntax/oracle/very_large_integers.6.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.6.res.oracle
@@ -1,11 +1,10 @@
[kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
-[kernel] tests/syntax/very_large_integers.c:53: User Error:
- Invalid attribute constant: 0x80000000000000000
-[kernel] tests/syntax/very_large_integers.c:58: Warning:
- ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] tests/syntax/very_large_integers.c:58: Warning:
- ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
- (9223372036854775808) )
+[kernel] tests/syntax/very_large_integers.c:58: User Error:
+ integer constant too large in expression -9999999999999999999U
+[kernel] tests/syntax/very_large_integers.c:58: User Error:
+ integer constant too large in expression 9999999999999999999U
+[kernel] tests/syntax/very_large_integers.c:58: Failure:
+ INDEX_RANGE initialization designator is not a valid constant
[kernel] User Error: stopping on file "tests/syntax/very_large_integers.c" that has errors. Add
'-kernel-msg-key pp' for preprocessing command.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/very_large_integers.7.res.oracle b/tests/syntax/oracle/very_large_integers.7.res.oracle
index 75dbebc66e69abf8a3bedb63843d538f6957ce7c..8596345066edd3425d844d951235ff397ce10030 100644
--- a/tests/syntax/oracle/very_large_integers.7.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.7.res.oracle
@@ -1,10 +1,5 @@
[kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
-[kernel] tests/syntax/very_large_integers.c:58: Warning:
- ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] tests/syntax/very_large_integers.c:58: Warning:
- ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
- (9223372036854775808) )
-[kernel] Failure: Cannot represent logical integer in C: 9999999999999999999
+[kernel] tests/syntax/very_large_integers.c:62: Failure: INDEX_RANGE too large
[kernel] User Error: stopping on file "tests/syntax/very_large_integers.c" that has errors. Add
'-kernel-msg-key pp' for preprocessing command.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/very_large_integers.8.res.oracle b/tests/syntax/oracle/very_large_integers.8.res.oracle
index a0898661e147feeff6bc975032c9c15c8f0f9fd0..1224d1e701bb481761b21300b2f1b0f3b9240b4a 100644
--- a/tests/syntax/oracle/very_large_integers.8.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.8.res.oracle
@@ -1,11 +1,11 @@
[kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
-[kernel] tests/syntax/very_large_integers.c:58: Warning:
+[kernel] tests/syntax/very_large_integers.c:67: User Error:
+ Invalid attribute constant: 0x80000000000000000
+[kernel] tests/syntax/very_large_integers.c:72: Warning:
ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] tests/syntax/very_large_integers.c:58: Warning:
+[kernel] tests/syntax/very_large_integers.c:72: Warning:
ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
(9223372036854775808) )
-[kernel] tests/syntax/very_large_integers.c:71: Failure:
- Invalid digit 9 in integer literal '09876543210' in base 8.
[kernel] User Error: stopping on file "tests/syntax/very_large_integers.c" that has errors. Add
'-kernel-msg-key pp' for preprocessing command.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/very_large_integers.9.res.oracle b/tests/syntax/oracle/very_large_integers.9.res.oracle
index 9ed0fe33d85bcd2a4c2cbca98f244296c17a65c1..618a1ec1dc5ac39b5daebe1cc6f6b62bd200a295 100644
--- a/tests/syntax/oracle/very_large_integers.9.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.9.res.oracle
@@ -1,12 +1,10 @@
[kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
-[kernel] tests/syntax/very_large_integers.c:58: Warning:
+[kernel] tests/syntax/very_large_integers.c:72: Warning:
ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] tests/syntax/very_large_integers.c:58: Warning:
+[kernel] tests/syntax/very_large_integers.c:72: Warning:
ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
(9223372036854775808) )
-[kernel:annot-error] tests/syntax/very_large_integers.c:80: Warning:
- Invalid slevel directive. Ignoring code annotation
-[kernel] User Error: warning annot-error treated as fatal error.
+[kernel] Failure: Cannot represent logical integer in C: 9999999999999999999
[kernel] User Error: stopping on file "tests/syntax/very_large_integers.c" that has errors. Add
'-kernel-msg-key pp' for preprocessing command.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/very_large_integers.c b/tests/syntax/very_large_integers.c
index 80e80299c6dc82f3f76654a45efd9e587e1e307a..5e31b993a90f21f75549692e59ffca2741a7310b 100644
--- a/tests/syntax/very_large_integers.c
+++ b/tests/syntax/very_large_integers.c
@@ -4,20 +4,21 @@
STDOPT: #"-cpp-extra-args=-DBITFIELD"
STDOPT: #"-cpp-extra-args=-DARRAY_DECL"
STDOPT: #"-cpp-extra-args=-DCASE_RANGE"
+ STDOPT: #"-cpp-extra-args=-DCASE_RANGE2"
STDOPT: #"-cpp-extra-args=-DINIT_DESIGNATOR"
STDOPT: #"-cpp-extra-args=-DINIT_DESIGNATOR2"
STDOPT: #"-cpp-extra-args=-DRANGE_DESIGNATOR"
+ STDOPT: #"-cpp-extra-args=-DRANGE_DESIGNATOR2"
STDOPT: #"-cpp-extra-args=-DATTRIBUTE_CONSTANT"
STDOPT: #"-cpp-extra-args=-DLOGIC_CONSTANT"
STDOPT: #"-cpp-extra-args=-DLOGIC_CONSTANT_OCTAL"
- STDOPT: #"-cpp-extra-args=-DEVA_UNROLL -eva"
+ STDOPT: #"-cpp-extra-args=-DEVA_UNROLL -eva -kernel-warn-key annot-error=error"
STDOPT: #"-cpp-extra-args=-DCABS_DOWHILE"
EXIT: 0
STDOPT: #"-cpp-extra-args=-DUNROLL_PRAGMA"
*/
volatile int nondet;
-
#ifdef BITFIELD
struct st {
int bf:(999999999999999999+9999999999999999999);
@@ -34,6 +35,14 @@ unsigned long nondetul;
void case_range() {
switch (nondetul)
case 0 ... 9999999999999999999U:;
+ case 0 ... 199999999999999999U:;
+}
+#endif
+
+#ifdef CASE_RANGE2
+void case_range2() {
+ switch (nondet)
+ case 0 ... 10000000U:;
}
#endif
@@ -49,6 +58,11 @@ int arr3[1] = { [9999999999999999999U] = 42 };
int arr4[1] = { [-9999999999999999999U ... 9999999999999999999U] = 42 };
#endif
+#ifdef RANGE_DESIGNATOR2
+int widths[] = { [99999999999999999 ... 999999999999999999] = 2 };
+#endif
+
+
#ifdef ATTRIBUTE_CONSTANT
struct acst {
int a __attribute__((aligned(0x80000000000000000)));