diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index b5b1e8e6c8f05c82a117622a8d76381f1b1c85d5..3f31de7afada7a4f7628bedbe0d7fb0f398a5eeb 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -8550,6 +8550,9 @@ and doInit local_env asconst add_implicit_ensures preinit so acc initl =
"start index larger than end index in range initializer";
let rec loop (i: int) =
if i > last then restil
+ else
+ if last - i > 100_000 then
+ Kernel.fatal ~current:true "INDEX_RANGE too large"
else
(top (Cabs.ATINDEX_INIT(
{ expr_node = Cabs.CONSTANT(Cabs.CONST_INT(string_of_int i));
diff --git a/tests/syntax/oracle/very_large_integers.0.res.oracle b/tests/syntax/oracle/very_large_integers.0.res.oracle
index 1cba593f0dce09c90a5f83f9c00ee9a0bca5a655..5c399742978a1ec800d490ec91c6966e8ccbac11 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:23: User Error:
- integer constant too large in expression (unsigned long long)999999999999999999 + 9999999999999999999
[kernel] tests/syntax/very_large_integers.c:24: User Error:
+ integer constant too large in expression (unsigned long long)999999999999999999 + 9999999999999999999
+[kernel] tests/syntax/very_large_integers.c:25: User Error:
bitfield width is not a valid integer constant
-[kernel] tests/syntax/very_large_integers.c:67: Warning:
+[kernel] tests/syntax/very_large_integers.c:73: Warning:
ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] tests/syntax/very_large_integers.c:67: Warning:
+[kernel] tests/syntax/very_large_integers.c:73: 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 29f4d99b92870d25cf2e6d7e3c30eade2e4853ad..cdb3ec56dafa2a977e97442947d4247b65d4eb7c 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:30: User Error:
+[kernel] tests/syntax/very_large_integers.c:31: User Error:
Cannot represent the integer 99999999999999999999U
-[kernel] tests/syntax/very_large_integers.c:30: User Error:
+[kernel] tests/syntax/very_large_integers.c:31: User Error:
Cannot represent the integer 99999999999999999999U
-[kernel] tests/syntax/very_large_integers.c:67: Warning:
+[kernel] tests/syntax/very_large_integers.c:73: Warning:
ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] tests/syntax/very_large_integers.c:67: Warning:
+[kernel] tests/syntax/very_large_integers.c:73: 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 b9200fafcf732ad23e1790a1244f683c4077eb89..5ee077c31fad25ca872777da6511614d645997da 100644
--- a/tests/syntax/oracle/very_large_integers.10.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.10.res.oracle
@@ -1,15 +1,11 @@
[kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
-[kernel] tests/syntax/very_large_integers.c:67: Warning:
+[kernel] tests/syntax/very_large_integers.c:73: Warning:
ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] tests/syntax/very_large_integers.c:67: Warning:
+[kernel] tests/syntax/very_large_integers.c:73: Warning:
ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
(9223372036854775808) )
-[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:86: Warning:
- invalid loop unrolling parameter (-9999999999999999999); ignoring
-[kernel] User Error: warning annot-error treated as fatal error.
+[kernel] tests/syntax/very_large_integers.c:86: 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 650607ffad8afa91c6601c4fc79e3dc5b5c3d1d9..f34db553ef8c687e47299e28108dd501d96c45ca 100644
--- a/tests/syntax/oracle/very_large_integers.11.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.11.res.oracle
@@ -1,12 +1,15 @@
[kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
-[kernel] tests/syntax/very_large_integers.c:67: Warning:
+[kernel] tests/syntax/very_large_integers.c:73: Warning:
ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] tests/syntax/very_large_integers.c:67: Warning:
+[kernel] tests/syntax/very_large_integers.c:73: Warning:
ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
(9223372036854775808) )
-[kernel:annot-error] tests/syntax/very_large_integers.c:91: 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:92: Warning:
+ invalid loop unrolling parameter (-9999999999999999999); ignoring
[kernel] User Error: warning annot-error treated as fatal error.
-[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.12.res.oracle b/tests/syntax/oracle/very_large_integers.12.res.oracle
index ba0dd7c26f203cbaa3c59a884191c006248d1ba9..9bb488764f30da8e64503a7abf8066cf1b1d4d67 100644
--- a/tests/syntax/oracle/very_large_integers.12.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.12.res.oracle
@@ -1,11 +1,12 @@
[kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
-[kernel] tests/syntax/very_large_integers.c:67: Warning:
+[kernel] tests/syntax/very_large_integers.c:73: Warning:
ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] tests/syntax/very_large_integers.c:67: Warning:
+[kernel] tests/syntax/very_large_integers.c:73: Warning:
ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
(9223372036854775808) )
-[kernel] tests/syntax/very_large_integers.c:95: User Error:
- Invalid digit 9 in integer literal '09' in base 8.
+[kernel:annot-error] tests/syntax/very_large_integers.c:97: Warning:
+ Invalid slevel directive. Ignoring code annotation
+[kernel] User Error: warning annot-error treated as fatal error.
[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
index 29b15f32902d4b08969c58c31fb240c3e12a0fb0..9584d2c18576f0a79e5c1d44eabc5fc4d31937c6 100644
--- a/tests/syntax/oracle/very_large_integers.13.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.13.res.oracle
@@ -1,22 +1,11 @@
[kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
-[kernel] tests/syntax/very_large_integers.c:67: Warning:
+[kernel] tests/syntax/very_large_integers.c:73: Warning:
ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] tests/syntax/very_large_integers.c:67: Warning:
+[kernel] tests/syntax/very_large_integers.c:73: Warning:
ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
(9223372036854775808) )
-[kernel] tests/syntax/very_large_integers.c:100: 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] tests/syntax/very_large_integers.c:101: 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.14.res.oracle b/tests/syntax/oracle/very_large_integers.14.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..829956ff3f3e2a9e2afa67a1cec279d976dd413f
--- /dev/null
+++ b/tests/syntax/oracle/very_large_integers.14.res.oracle
@@ -0,0 +1,22 @@
+[kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
+[kernel] tests/syntax/very_large_integers.c:73: Warning:
+ ignoring invalid aligned attribute: __aligned__(9223372036854775808)
+[kernel] tests/syntax/very_large_integers.c:73: Warning:
+ ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
+ (9223372036854775808) )
+[kernel] tests/syntax/very_large_integers.c:106: 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 25740fed33da86b20117393d4a25f8919e975238..c4ae365bcb897e7ff07b062e76bd13ad9be003b1 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:37: User Error:
+[kernel] tests/syntax/very_large_integers.c:38: User Error:
integer constant too large in expression 9999999999999999999U
-[kernel] tests/syntax/very_large_integers.c:37: Failure:
+[kernel] tests/syntax/very_large_integers.c:38: 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 f4cbe4f4e6d14e2acf9f68cbbcc46c39d8f90a12..d98169ad396e6838f395474e8250f54869322a9f 100644
--- a/tests/syntax/oracle/very_large_integers.3.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.3.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
-[kernel] tests/syntax/very_large_integers.c:45: Failure: Case range too large
+[kernel] tests/syntax/very_large_integers.c:46: 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 e53651c2f5bff8cd11135c4216465253a4faf8c0..cb6369a167f6747284f2277d84fc8e4a5812d3b8 100644
--- a/tests/syntax/oracle/very_large_integers.4.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.4.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
-[kernel] tests/syntax/very_large_integers.c:50: Failure:
+[kernel] tests/syntax/very_large_integers.c:51: 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.
diff --git a/tests/syntax/oracle/very_large_integers.5.res.oracle b/tests/syntax/oracle/very_large_integers.5.res.oracle
index 028afa06f27e1524caf054410fd66a022790e970..581438ce1def565d1848d039503967de248d7275 100644
--- a/tests/syntax/oracle/very_large_integers.5.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.5.res.oracle
@@ -1,12 +1,12 @@
[kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
-[kernel] tests/syntax/very_large_integers.c:54: User Error:
+[kernel] tests/syntax/very_large_integers.c:55: User Error:
INDEX initialization designator overflows
- 52
- 53 #ifdef INIT_DESIGNATOR2
- 54 int arr3[1] = { [9999999999999999999U] = 42 };
+ 53
+ 54 #ifdef INIT_DESIGNATOR2
+ 55 int arr3[1] = { [9999999999999999999U] = 42 };
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- 55 #endif
- 56
+ 56 #endif
+ 57
[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 80ea4f9cf539e9e3643304efad8bd4760c7ffb06..c0200e81a9cb45e99d52ce56e984f60d27f0fb6e 100644
--- a/tests/syntax/oracle/very_large_integers.6.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.6.res.oracle
@@ -1,9 +1,9 @@
[kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
-[kernel] tests/syntax/very_large_integers.c:58: User Error:
+[kernel] tests/syntax/very_large_integers.c:59: User Error:
integer constant too large in expression -9999999999999999999U
-[kernel] tests/syntax/very_large_integers.c:58: User Error:
+[kernel] tests/syntax/very_large_integers.c:59: User Error:
integer constant too large in expression 9999999999999999999U
-[kernel] tests/syntax/very_large_integers.c:58: Failure:
+[kernel] tests/syntax/very_large_integers.c:59: 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.
diff --git a/tests/syntax/oracle/very_large_integers.7.res.oracle b/tests/syntax/oracle/very_large_integers.7.res.oracle
index c998aaf5b33f994a1864b4fe96397055cc29680c..c6d72b6acf3b8292436a4244502e8b27fbdb22ac 100644
--- a/tests/syntax/oracle/very_large_integers.7.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.7.res.oracle
@@ -1,11 +1,5 @@
[kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
-[kernel] tests/syntax/very_large_integers.c:62: User Error:
- Invalid attribute constant: 0x80000000000000000
-[kernel] tests/syntax/very_large_integers.c:67: Warning:
- ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] tests/syntax/very_large_integers.c:67: Warning:
- ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
- (9223372036854775808) )
+[kernel] tests/syntax/very_large_integers.c:63: 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 1028d33119a6f9eb712dfddbf7ec633b15687f19..a78f4c463c94bbc8b4958e94d83abc81fc9cdfd7 100644
--- a/tests/syntax/oracle/very_large_integers.8.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.8.res.oracle
@@ -1,10 +1,11 @@
[kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
-[kernel] tests/syntax/very_large_integers.c:67: Warning:
+[kernel] tests/syntax/very_large_integers.c:68: User Error:
+ Invalid attribute constant: 0x80000000000000000
+[kernel] tests/syntax/very_large_integers.c:73: Warning:
ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] tests/syntax/very_large_integers.c:67: Warning:
+[kernel] tests/syntax/very_large_integers.c:73: Warning:
ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
(9223372036854775808) )
-[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/oracle/very_large_integers.9.res.oracle b/tests/syntax/oracle/very_large_integers.9.res.oracle
index bcf3568e2a81f29b18bf9151dbacbf558a0d1890..298b469609ed8c5f53c216d25a6d6edf23eace44 100644
--- a/tests/syntax/oracle/very_large_integers.9.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.9.res.oracle
@@ -1,11 +1,10 @@
[kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
-[kernel] tests/syntax/very_large_integers.c:67: Warning:
+[kernel] tests/syntax/very_large_integers.c:73: Warning:
ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] tests/syntax/very_large_integers.c:67: Warning:
+[kernel] tests/syntax/very_large_integers.c:73: Warning:
ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
(9223372036854775808) )
-[kernel] tests/syntax/very_large_integers.c:80: Failure:
- Invalid digit 9 in integer literal '09876543210' in base 8.
+[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 47c3629e67cfda6cca3d3f839734c8ae167c29dd..424fe4aea35b7e21a036703a00635311928517f5 100644
--- a/tests/syntax/very_large_integers.c
+++ b/tests/syntax/very_large_integers.c
@@ -8,6 +8,7 @@
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"
@@ -40,7 +41,7 @@ void case_range() {
#endif
#ifdef CASE_RANGE2
-void case_range() {
+void case_range2() {
switch (nondet)
case 0 ... 10000000U:;
}
@@ -58,6 +59,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)));