diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 06d74aa1d67bc6ffca2692da322921dea0aa1d41..5debe483a4b49eecd320cef4bdb874053798ff43 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -3384,7 +3384,13 @@ let rec setOneInit this o preinit =
let pMaxIdx, pArray =
match this with
| NoInitPre -> (* No initializer so far here *)
- ref idx, ref (Array.make (max 32 (idx + 1)) NoInitPre)
+ begin
+ try
+ ref idx, ref (Array.make (max 32 (idx + 1)) NoInitPre)
+ with Invalid_argument _ | Out_of_memory ->
+ Kernel.abort ~current:true
+ "array length too large: %d" ((max 32 (idx + 1)))
+ end
| CompoundPre (pMaxIdx, pArray) ->
if !pMaxIdx < idx then begin
diff --git a/tests/syntax/oracle/very_large_integers.0.res.oracle b/tests/syntax/oracle/very_large_integers.0.res.oracle
index db47193a76d6e1bfe1ae750ac1ab111463eb03be..070b0b0891f16262542a70f19eb56aace59d771e 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 very_large_integers.c (with preprocessing)
-[kernel] very_large_integers.c:23: User Error:
+[kernel] very_large_integers.c:25: User Error:
integer constant too large in expression (unsigned long long)999999999999999999 + 9999999999999999999
-[kernel] very_large_integers.c:24: User Error:
+[kernel] very_large_integers.c:26: User Error:
bitfield width is not a valid integer constant
-[kernel] very_large_integers.c:72: Warning:
+[kernel] very_large_integers.c:74: Warning:
ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] very_large_integers.c:72: Warning:
+[kernel] very_large_integers.c:74: Warning:
ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
(9223372036854775808) )
[kernel] User Error: stopping on file "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 307887ca5d2b21c81d4219ce0aff720be6d45899..0ceeff36ccde04c3d61ff573c96102096722534f 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 very_large_integers.c (with preprocessing)
-[kernel] very_large_integers.c:30: User Error:
+[kernel] very_large_integers.c:32: User Error:
Cannot represent the integer 99999999999999999999U
-[kernel] very_large_integers.c:30: User Error:
+[kernel] very_large_integers.c:32: User Error:
Cannot represent the integer 99999999999999999999U
-[kernel] very_large_integers.c:72: Warning:
+[kernel] very_large_integers.c:74: Warning:
ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] very_large_integers.c:72: Warning:
+[kernel] very_large_integers.c:74: Warning:
ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
(9223372036854775808) )
[kernel] User Error: stopping on file "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 12b104249f7108e741dbdcbaf168b0c5e4e460c8..468e5fb2083acf41ff3217f2eb0a4afcbb5e4412 100644
--- a/tests/syntax/oracle/very_large_integers.10.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.10.res.oracle
@@ -1,10 +1,10 @@
[kernel] Parsing very_large_integers.c (with preprocessing)
-[kernel] very_large_integers.c:72: Warning:
+[kernel] very_large_integers.c:74: Warning:
ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] very_large_integers.c:72: Warning:
+[kernel] very_large_integers.c:74: Warning:
ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
(9223372036854775808) )
-[kernel] very_large_integers.c:85: Failure:
+[kernel] very_large_integers.c:87: Failure:
Invalid digit 9 in integer literal '09876543210' in base 8.
[kernel] User Error: stopping on file "very_large_integers.c" that has errors. Add
'-kernel-msg-key pp' for preprocessing command.
diff --git a/tests/syntax/oracle/very_large_integers.11.res.oracle b/tests/syntax/oracle/very_large_integers.11.res.oracle
index 475579421115b3243ca7789a42b46a43b5ad8efc..c0fab3ffc4147ea4527558d6d2590660893ad8cf 100644
--- a/tests/syntax/oracle/very_large_integers.11.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.11.res.oracle
@@ -1,19 +1,19 @@
[kernel] Parsing very_large_integers.c (with preprocessing)
-[kernel] very_large_integers.c:72: Warning:
+[kernel] very_large_integers.c:74: Warning:
ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] very_large_integers.c:72: Warning:
+[kernel] very_large_integers.c:74: Warning:
ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
(9223372036854775808) )
-[kernel:annot-error] very_large_integers.c:94: Warning:
+[kernel:annot-error] very_large_integers.c:114: 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] very_large_integers.c:91: Warning:
+[kernel:annot-error] very_large_integers.c:111: Warning:
invalid loop unrolling parameter; ignoring
-[kernel:annot-error] very_large_integers.c:93: Warning:
+[kernel:annot-error] very_large_integers.c:113: Warning:
invalid loop unrolling parameter; ignoring
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
diff --git a/tests/syntax/oracle/very_large_integers.12.res.oracle b/tests/syntax/oracle/very_large_integers.12.res.oracle
index bfe4d557fd5884566eae8264163769c4f9568f84..71f4141e2feac45abe01a04d0e72485ae2fbbfda 100644
--- a/tests/syntax/oracle/very_large_integers.12.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.12.res.oracle
@@ -1,10 +1,10 @@
[kernel] Parsing very_large_integers.c (with preprocessing)
-[kernel] very_large_integers.c:72: Warning:
+[kernel] very_large_integers.c:74: Warning:
ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] very_large_integers.c:72: Warning:
+[kernel] very_large_integers.c:74: Warning:
ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
(9223372036854775808) )
-[kernel] very_large_integers.c:98: User Error:
+[kernel] very_large_integers.c:118: User Error:
Invalid digit 9 in integer literal '09' in base 8.
[kernel] User Error: stopping on file "very_large_integers.c" that has errors. Add
'-kernel-msg-key pp' for preprocessing command.
diff --git a/tests/syntax/oracle/very_large_integers.13.res.oracle b/tests/syntax/oracle/very_large_integers.13.res.oracle
index 2ae16ad88a397319ee4843017e4b397a22b8b1ca..3d0eb837dc4c63ebeadb4d593353cddca2ad52dd 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 very_large_integers.c (with preprocessing)
-[kernel] very_large_integers.c:72: Warning:
+[kernel] very_large_integers.c:74: Warning:
ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] very_large_integers.c:72: Warning:
+[kernel] very_large_integers.c:74: Warning:
ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
(9223372036854775808) )
-[kernel] 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;
-}
-
-
+[kernel] very_large_integers.c:92: User Error:
+ array length too large: 72057594037927937
+[kernel] User Error: stopping on file "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..d404452dfd895f433aa72dea49482f99e8643a49
--- /dev/null
+++ b/tests/syntax/oracle/very_large_integers.14.res.oracle
@@ -0,0 +1,11 @@
+[kernel] Parsing very_large_integers.c (with preprocessing)
+[kernel] very_large_integers.c:74: Warning:
+ ignoring invalid aligned attribute: __aligned__(9223372036854775808)
+[kernel] very_large_integers.c:74: Warning:
+ ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
+ (9223372036854775808) )
+[kernel] very_large_integers.c:103: User Error:
+ array length too large: 7205759403792794
+[kernel] User Error: stopping on file "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.15.res.oracle b/tests/syntax/oracle/very_large_integers.15.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..dc363357b8e0127f7ae9529b4746e8c6280c06d0
--- /dev/null
+++ b/tests/syntax/oracle/very_large_integers.15.res.oracle
@@ -0,0 +1,22 @@
+[kernel] Parsing very_large_integers.c (with preprocessing)
+[kernel] very_large_integers.c:74: Warning:
+ ignoring invalid aligned attribute: __aligned__(9223372036854775808)
+[kernel] very_large_integers.c:74: Warning:
+ ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
+ (9223372036854775808) )
+[kernel] very_large_integers.c:123: 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 e66ed1591681d53e53f404a32095556d54bd2cf0..1b64027503125bcc49fc9d4599971c336cfb15b1 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 very_large_integers.c (with preprocessing)
-[kernel] very_large_integers.c:37: User Error:
+[kernel] very_large_integers.c:39: User Error:
integer constant too large in expression 9999999999999999999U
-[kernel] very_large_integers.c:37: Failure:
+[kernel] very_large_integers.c:39: Failure:
Cannot understand the constants in case range
[kernel] User Error: stopping on file "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 e98fe85d7ff380c6be85e8ce79137c9709721ddf..09f3e166f6fc16b424d6b82504c8e6acbd5ba5c2 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 very_large_integers.c (with preprocessing)
-[kernel] very_large_integers.c:45: Failure: Case range too large
+[kernel] very_large_integers.c:47: Failure: Case range too large
[kernel] User Error: stopping on file "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 5af290bef311d47b04e339ebb7247767c84c5d15..817f524174fd43a32cf9ba39381ad802b66061ee 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 very_large_integers.c (with preprocessing)
-[kernel] very_large_integers.c:50: Failure:
+[kernel] very_large_integers.c:52: Failure:
Array length 9999999999999999999U is not a compile-time constant: no explicit initializer allowed.
[kernel] User Error: stopping on file "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 5dbd30727bd1b94363fb985f0185ba755e8d10a9..e38af09ec48d06731752da54ed19b9dcfb554195 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 very_large_integers.c (with preprocessing)
-[kernel] very_large_integers.c:54: User Error:
+[kernel] very_large_integers.c:56: User Error:
INDEX initialization designator overflows
- 52
- 53 #ifdef INIT_DESIGNATOR2
- 54 int arr3[1] = { [9999999999999999999U] = 42 };
+ 54
+ 55 #ifdef INIT_DESIGNATOR2
+ 56 int arr3[1] = { [9999999999999999999U] = 42 };
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- 55 #endif
- 56
+ 57 #endif
+ 58
[kernel] User Error: stopping on file "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 8b2be7f122e514e8fef4b2dd02ab1b20fb1937d6..dd10e931b3a969b30c76a65f4809e6a6cc45855e 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 very_large_integers.c (with preprocessing)
-[kernel] very_large_integers.c:58: User Error:
+[kernel] very_large_integers.c:60: User Error:
integer constant too large in expression -9999999999999999999U
-[kernel] very_large_integers.c:58: User Error:
+[kernel] very_large_integers.c:60: User Error:
integer constant too large in expression 9999999999999999999U
-[kernel] very_large_integers.c:58: Failure:
+[kernel] very_large_integers.c:60: Failure:
INDEX_RANGE initialization designator is not a valid constant
[kernel] User Error: stopping on file "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 90e6c755d4504902ac707708502a65d7b2f87c07..406e636f4628df47d7cbd15e4cb0569b412feddc 100644
--- a/tests/syntax/oracle/very_large_integers.7.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.7.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing very_large_integers.c (with preprocessing)
-[kernel] very_large_integers.c:62: Failure: INDEX_RANGE too large
+[kernel] very_large_integers.c:64: Failure: INDEX_RANGE too large
[kernel] User Error: stopping on file "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 5eae6db9af1673c5803806b309d729f9b543b668..8de4f1b1a653361bea91ef257e180702797f46ce 100644
--- a/tests/syntax/oracle/very_large_integers.8.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.8.res.oracle
@@ -1,9 +1,9 @@
[kernel] Parsing very_large_integers.c (with preprocessing)
-[kernel] very_large_integers.c:67: User Error:
+[kernel] very_large_integers.c:69: User Error:
Invalid attribute constant: 0x80000000000000000
-[kernel] very_large_integers.c:72: Warning:
+[kernel] very_large_integers.c:74: Warning:
ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] very_large_integers.c:72: Warning:
+[kernel] very_large_integers.c:74: Warning:
ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
(9223372036854775808) )
[kernel] User Error: stopping on file "very_large_integers.c" that has errors. Add
diff --git a/tests/syntax/oracle/very_large_integers.9.res.oracle b/tests/syntax/oracle/very_large_integers.9.res.oracle
index e1237274ec9f58c32d41c55492aafb860b7ff0f8..fb843772ce75ca63700e1629a728e82e4f660024 100644
--- a/tests/syntax/oracle/very_large_integers.9.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.9.res.oracle
@@ -1,7 +1,7 @@
[kernel] Parsing very_large_integers.c (with preprocessing)
-[kernel] very_large_integers.c:72: Warning:
+[kernel] very_large_integers.c:74: Warning:
ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] very_large_integers.c:72: Warning:
+[kernel] very_large_integers.c:74: Warning:
ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
(9223372036854775808) )
[kernel] Failure: Cannot represent logical integer in C: 9999999999999999999
diff --git a/tests/syntax/very_large_integers.c b/tests/syntax/very_large_integers.c
index 5e31b993a90f21f75549692e59ffca2741a7310b..996c0ca0bf0ce2528d4ebb0cd4fe8801b4426e67 100644
--- a/tests/syntax/very_large_integers.c
+++ b/tests/syntax/very_large_integers.c
@@ -14,6 +14,8 @@
STDOPT: #"-cpp-extra-args=-DLOGIC_CONSTANT_OCTAL"
STDOPT: #"-cpp-extra-args=-DEVA_UNROLL -eva -kernel-warn-key annot-error=error"
STDOPT: #"-cpp-extra-args=-DCABS_DOWHILE"
+ STDOPT: #"-cpp-extra-args=-DARRAY_INIT1"
+ STDOPT: #"-cpp-extra-args=-DARRAY_INIT2"
EXIT: 0
STDOPT: #"-cpp-extra-args=-DUNROLL_PRAGMA"
*/
@@ -85,6 +87,24 @@ typedef struct {
//@ type too_large_logic_array_octal = int[09876543210];
#endif
+#ifdef ARRAY_INIT1
+// Previously caused Invalid_argument(Array.make)
+int a1[] = {[72057594037927936] = 0};
+#endif
+
+#ifdef ARRAY_INIT2
+struct arri2 {
+ int a[7205759403792795];
+};
+struct st {
+ struct arri2 a;
+};
+// Previously caused Out of memory
+struct st s = {
+ {{[7205759403792793 ... 7205759403792793] = 0}}
+};
+#endif
+
int main() {
#ifdef EVA_UNROLL
//@ loop unroll (-9999999999999999999); // IntLimit