diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index f6aebe306d45681b089a7e5e8c08a75260f7e139..f958082d4b04d4d907094cd9ea3fefcb985d5284 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -3399,9 +3399,13 @@ let rec setOneInit this o preinit =
let l = Array.length !pArray in
if l <= idx then begin
let growBy = max (max 32 (idx + 1 - l)) (l / 2) in
- let newarray = Array.make (growBy + idx) NoInitPre in
- Array.blit !pArray 0 newarray 0 l;
- pArray := newarray
+ try
+ let newarray = Array.make (growBy + idx) NoInitPre in
+ Array.blit !pArray 0 newarray 0 l;
+ pArray := newarray
+ with Invalid_argument _ | Out_of_memory ->
+ Kernel.abort ~current:true
+ "array length too large for Frama-C: %d" (idx)
end
end;
pMaxIdx, pArray
diff --git a/tests/syntax/oracle/very_large_integers.0.res.oracle b/tests/syntax/oracle/very_large_integers.0.res.oracle
index 1236cc7d7251b2e8c568575ebd87c1f5fe81ecbc..aadc000d33d4ccd15c6d6c8d5d00427c21ff79cd 100644
--- a/tests/syntax/oracle/very_large_integers.0.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.0.res.oracle
@@ -1,7 +1,7 @@
[kernel] Parsing very_large_integers.c (with preprocessing)
-[kernel] very_large_integers.c:25: User Error:
+[kernel] very_large_integers.c:35: User Error:
integer constant too large in expression (unsigned long long)999999999999999999 + 9999999999999999999
-[kernel] very_large_integers.c:26: User Error:
+[kernel] very_large_integers.c:36: User Error:
bitfield width is not a valid integer 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.1.res.oracle b/tests/syntax/oracle/very_large_integers.1.res.oracle
index 0ceeff36ccde04c3d61ff573c96102096722534f..4f4479d850994060abd17b9c1bb2c03213580381 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:32: User Error:
+[kernel] very_large_integers.c:42: User Error:
Cannot represent the integer 99999999999999999999U
-[kernel] very_large_integers.c:32: User Error:
+[kernel] very_large_integers.c:42: User Error:
Cannot represent the integer 99999999999999999999U
-[kernel] very_large_integers.c:74: Warning:
+[kernel] very_large_integers.c:84: Warning:
ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] very_large_integers.c:74: Warning:
+[kernel] very_large_integers.c:84: 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 468e5fb2083acf41ff3217f2eb0a4afcbb5e4412..b40b28536c462ed1cdf6e67e9bd4a8662508186b 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:74: Warning:
+[kernel] very_large_integers.c:84: Warning:
ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] very_large_integers.c:74: Warning:
+[kernel] very_large_integers.c:84: Warning:
ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
(9223372036854775808) )
-[kernel] very_large_integers.c:87: Failure:
+[kernel] very_large_integers.c:97: 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 c0fab3ffc4147ea4527558d6d2590660893ad8cf..26c3f665ecafde3a0756a18e39bff27fc10983c1 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:74: Warning:
+[kernel] very_large_integers.c:84: Warning:
ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] very_large_integers.c:74: Warning:
+[kernel] very_large_integers.c:84: Warning:
ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
(9223372036854775808) )
-[kernel:annot-error] very_large_integers.c:114: Warning:
+[kernel:annot-error] very_large_integers.c:132: 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:111: Warning:
+[kernel:annot-error] very_large_integers.c:129: Warning:
invalid loop unrolling parameter; ignoring
-[kernel:annot-error] very_large_integers.c:113: Warning:
+[kernel:annot-error] very_large_integers.c:131: 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 71f4141e2feac45abe01a04d0e72485ae2fbbfda..8b9b72707ecc9fd6c21a7915fd0c220d2c065b3f 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:74: Warning:
+[kernel] very_large_integers.c:84: Warning:
ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] very_large_integers.c:74: Warning:
+[kernel] very_large_integers.c:84: Warning:
ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
(9223372036854775808) )
-[kernel] very_large_integers.c:118: User Error:
+[kernel] very_large_integers.c:136: 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 3d0eb837dc4c63ebeadb4d593353cddca2ad52dd..3a4a0c0b8384464f300e6e536aa0a235f44df597 100644
--- a/tests/syntax/oracle/very_large_integers.13.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.13.res.oracle
@@ -1,10 +1,10 @@
[kernel] Parsing very_large_integers.c (with preprocessing)
-[kernel] very_large_integers.c:74: Warning:
+[kernel] very_large_integers.c:84: Warning:
ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] very_large_integers.c:74: Warning:
+[kernel] very_large_integers.c:84: Warning:
ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
(9223372036854775808) )
-[kernel] very_large_integers.c:92: User Error:
+[kernel] very_large_integers.c:102: 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.
diff --git a/tests/syntax/oracle/very_large_integers.14.res.oracle b/tests/syntax/oracle/very_large_integers.14.res.oracle
index d404452dfd895f433aa72dea49482f99e8643a49..8d7684b496fc3074cacf1497a58a1b93f44243ed 100644
--- a/tests/syntax/oracle/very_large_integers.14.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.14.res.oracle
@@ -1,10 +1,10 @@
[kernel] Parsing very_large_integers.c (with preprocessing)
-[kernel] very_large_integers.c:74: Warning:
+[kernel] very_large_integers.c:84: Warning:
ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] very_large_integers.c:74: Warning:
+[kernel] very_large_integers.c:84: Warning:
ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
(9223372036854775808) )
-[kernel] very_large_integers.c:103: User Error:
+[kernel] very_large_integers.c:113: 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.
diff --git a/tests/syntax/oracle/very_large_integers.15.res.oracle b/tests/syntax/oracle/very_large_integers.15.res.oracle
index dc363357b8e0127f7ae9529b4746e8c6280c06d0..adad50468228f08fd7b086a7df5e94d996d82dbe 100644
--- a/tests/syntax/oracle/very_large_integers.15.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.15.res.oracle
@@ -1,22 +1,11 @@
[kernel] Parsing very_large_integers.c (with preprocessing)
-[kernel] very_large_integers.c:74: Warning:
+[kernel] very_large_integers.c:84: Warning:
ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] very_large_integers.c:74: Warning:
+[kernel] very_large_integers.c:84: 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;
-}
-
-
+[kernel] very_large_integers.c:119: User Error:
+ array length too large for Frama-C: 72057594037927936
+[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.16.res.oracle b/tests/syntax/oracle/very_large_integers.16.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..1d8fc3c7d7c010cb51c88aa883b1d8d7426f8e48
--- /dev/null
+++ b/tests/syntax/oracle/very_large_integers.16.res.oracle
@@ -0,0 +1,11 @@
+[kernel] Parsing very_large_integers.c (with preprocessing)
+[kernel] very_large_integers.c:84: Warning:
+ ignoring invalid aligned attribute: __aligned__(9223372036854775808)
+[kernel] very_large_integers.c:84: Warning:
+ ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
+ (9223372036854775808) )
+[kernel] very_large_integers.c:123: User Error:
+ array length too large for Frama-C: 7205759403792793
+[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.17.res.oracle b/tests/syntax/oracle/very_large_integers.17.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..3012ddb57d4c817230e4b623ba1731f31374dd26
--- /dev/null
+++ b/tests/syntax/oracle/very_large_integers.17.res.oracle
@@ -0,0 +1,22 @@
+[kernel] Parsing very_large_integers.c (with preprocessing)
+[kernel] very_large_integers.c:84: Warning:
+ ignoring invalid aligned attribute: __aligned__(9223372036854775808)
+[kernel] very_large_integers.c:84: Warning:
+ ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
+ (9223372036854775808) )
+[kernel] very_large_integers.c:141: 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 1b64027503125bcc49fc9d4599971c336cfb15b1..851e81eb0347ab34fc53a305992e740c3faed63b 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:39: User Error:
+[kernel] very_large_integers.c:49: User Error:
integer constant too large in expression 9999999999999999999U
-[kernel] very_large_integers.c:39: Failure:
+[kernel] very_large_integers.c:49: 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 09f3e166f6fc16b424d6b82504c8e6acbd5ba5c2..b46e1c5c2cdc38eb7172f8fac3c72b50af75f6c1 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:47: Failure: Case range too large
+[kernel] very_large_integers.c:57: 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 b4a00ef7aed6589641454c16903b943c79833606..5e6c8b87f5192cbca50ffe3fb8ef83cb69bb860b 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:52: User Error:
+[kernel] very_large_integers.c:62: User Error:
Array length 9999999999999999999U is too big: 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 e38af09ec48d06731752da54ed19b9dcfb554195..4d011e9d84409f07345491a9d08de690be085027 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:56: User Error:
+[kernel] very_large_integers.c:66: User Error:
INDEX initialization designator overflows
- 54
- 55 #ifdef INIT_DESIGNATOR2
- 56 int arr3[1] = { [9999999999999999999U] = 42 };
+ 64
+ 65 #ifdef INIT_DESIGNATOR2
+ 66 int arr3[1] = { [9999999999999999999U] = 42 };
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- 57 #endif
- 58
+ 67 #endif
+ 68
[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 dd10e931b3a969b30c76a65f4809e6a6cc45855e..c603644b586085db6acb633701ae40c06a261e5f 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:60: User Error:
+[kernel] very_large_integers.c:70: User Error:
integer constant too large in expression -9999999999999999999U
-[kernel] very_large_integers.c:60: User Error:
+[kernel] very_large_integers.c:70: User Error:
integer constant too large in expression 9999999999999999999U
-[kernel] very_large_integers.c:60: Failure:
+[kernel] very_large_integers.c:70: 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 406e636f4628df47d7cbd15e4cb0569b412feddc..5ca8f61644c59e35ad6866a23f53a401e46009c8 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:64: Failure: INDEX_RANGE too large
+[kernel] very_large_integers.c:74: 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 8de4f1b1a653361bea91ef257e180702797f46ce..bf9a096053416e2ccb7778ba85efc209edc8d656 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:69: User Error:
+[kernel] very_large_integers.c:79: User Error:
Invalid attribute constant: 0x80000000000000000
-[kernel] very_large_integers.c:74: Warning:
+[kernel] very_large_integers.c:84: Warning:
ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] very_large_integers.c:74: Warning:
+[kernel] very_large_integers.c:84: 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 fb843772ce75ca63700e1629a728e82e4f660024..2c2a6cbdf3ab7e69653f75f37b88839bf91fe53d 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:74: Warning:
+[kernel] very_large_integers.c:84: Warning:
ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] very_large_integers.c:74: Warning:
+[kernel] very_large_integers.c:84: 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 996c0ca0bf0ce2528d4ebb0cd4fe8801b4426e67..02f67ae756044c9e232212160f82af45e9017f32 100644
--- a/tests/syntax/very_large_integers.c
+++ b/tests/syntax/very_large_integers.c
@@ -16,10 +16,20 @@
STDOPT: #"-cpp-extra-args=-DCABS_DOWHILE"
STDOPT: #"-cpp-extra-args=-DARRAY_INIT1"
STDOPT: #"-cpp-extra-args=-DARRAY_INIT2"
+ STDOPT: #"-cpp-extra-args=-DARRAY_INIT3"
+ STDOPT: #"-cpp-extra-args=-DARRAY_INIT4"
EXIT: 0
STDOPT: #"-cpp-extra-args=-DUNROLL_PRAGMA"
*/
+
+
+
+
+
+
+// Lines intentionally left blank to minimize future oracle changes
+
volatile int nondet;
#ifdef BITFIELD
struct st {
@@ -105,6 +115,14 @@ struct st s = {
};
#endif
+#ifdef ARRAY_INIT3
+int ai3[] = {0xdead, [72057594037927936] = 0xbeef};
+#endif
+#ifdef ARRAY_INIT4
+// Previously caused Out of memory
+int ai4[] = {1, [7205759403792793] = 11};
+#endif
+
int main() {
#ifdef EVA_UNROLL
//@ loop unroll (-9999999999999999999); // IntLimit