diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 06d74aa1d67bc6ffca2692da322921dea0aa1d41..43fd613d1c2e2e3054354427aca69d004114f5c7 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
@@ -3763,11 +3769,11 @@ let integerArrayLength (leno: exp option) : int =
| None -> max_int
| Some len ->
try lenOfArray leno
- with LenOfArray ->
- Kernel.fatal ~current:true
- "Array length %a is not a compile-time constant: \
- no explicit initializer allowed."
- Cil_printer.pp_exp len
+ with
+ | LenOfArray cause ->
+ Kernel.abort ~current:true
+ "Array length %a is %a: no explicit initializer allowed."
+ Cil_printer.pp_exp len Cil.pp_incorrect_array_length cause
let find_field_offset cond (fidlist: fieldinfo list) : offset =
(* Depth first search for the field. This appears to be what GCC does.
diff --git a/src/kernel_services/analysis/bit_utils.ml b/src/kernel_services/analysis/bit_utils.ml
index 779bf41c4668613aca904c989869c9f84de04235..fd7780682e92a364e79922d1b1288d2eeaa3c56a 100644
--- a/src/kernel_services/analysis/bit_utils.ml
+++ b/src/kernel_services/analysis/bit_utils.ml
@@ -471,7 +471,7 @@ let rec type_compatible t1 t2 =
| TArray (t1', s1, _), TArray (t2', s2, _) ->
type_compatible t1' t2' &&
(s1 == s2 || try Integer.equal (Cil.lenOfArray64 s1) (Cil.lenOfArray64 s2)
- with Cil.LenOfArray -> false)
+ with Cil.LenOfArray _ -> false)
| TFun (r1, a1, v1, _), TFun (r2, a2, v2, _) ->
v1 = v2 && type_compatible r1 r2 &&
(match a1, a2 with
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 705f2c39c7a471b53903976e05469a354f88a085..e4e407d1b53294b1407b8543a8c85cbfc9e97ac2 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -6047,19 +6047,30 @@ let increm64 (e: exp) i =
false
(new_exp ~loc:e.eloc (BinOp(bop, e, kinteger64 ~loc:e.eloc i, et)))
-exception LenOfArray
+type incorrect_array_length = Not_constant | Not_integer | Negative | Too_big
+
+let pp_incorrect_array_length fmt = function
+ | Not_constant -> Format.pp_print_string fmt "not a compile-time constant"
+ | Negative -> Format.pp_print_string fmt "negative"
+ | Not_integer -> Format.pp_print_string fmt "not an integral constant"
+ | Too_big -> Format.pp_print_string fmt "too big"
+
+exception LenOfArray of incorrect_array_length
+
let lenOfArray64 eo =
match eo with
- None -> raise LenOfArray
+ None -> raise (LenOfArray Not_constant)
| Some e -> begin
match (constFold true e).enode with
| Const(CInt64(ni, _, _)) when Integer.ge ni Integer.zero ->
ni
- | _ -> raise LenOfArray
+ | Const(CInt64 _) -> raise (LenOfArray Negative)
+ | Const _ -> raise (LenOfArray Not_integer)
+ | _ -> raise (LenOfArray Not_constant)
end
let lenOfArray eo =
match Integer.to_int_opt (lenOfArray64 eo) with
- | None -> raise LenOfArray
+ | None -> raise (LenOfArray Too_big)
| Some l -> l
(*** Make an initializer for zeroing a data type ***)
diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli
index b7fb1ce9064956baea8bc0a2a4ae21ec5b6e6194..ebc091d0c73d33cbebd9b3ef0f88048ed2c3dc21 100644
--- a/src/kernel_services/ast_queries/cil.mli
+++ b/src/kernel_services/ast_queries/cil.mli
@@ -613,10 +613,17 @@ val isArrayType: typ -> bool
(** True if the argument is a struct of union type *)
val isStructOrUnionType: typ -> bool
+(** possible causes for raising {!Cil.LenOfArray} *)
+type incorrect_array_length = Not_constant | Not_integer | Negative | Too_big
+
+val pp_incorrect_array_length:
+ Format.formatter -> incorrect_array_length -> unit
+
(** Raised when {!Cil.lenOfArray} fails either because the length is [None],
* because it is a non-constant expression, or because it overflows an int.
*)
-exception LenOfArray
+exception LenOfArray of incorrect_array_length
+
(** Call to compute the array length as present in the array type, to an
* integer. Raises {!Cil.LenOfArray} if not able to compute the length, such
diff --git a/src/plugins/e-acsl/src/code_generator/logic_array.ml b/src/plugins/e-acsl/src/code_generator/logic_array.ml
index 0a8733cbafaec3454019096110574b22c9853c74..13ff7de6305750c99ec6125c23d0bb9aa1bf2508 100644
--- a/src/plugins/e-acsl/src/code_generator/logic_array.ml
+++ b/src/plugins/e-acsl/src/code_generator/logic_array.ml
@@ -46,7 +46,7 @@ let length_exp ~loc kf env ~name array =
try
let len = Cil.lenOfArray64 array_len in
(Cil.kinteger64 ~loc len), env
- with Cil.LenOfArray ->
+ with Cil.LenOfArray _ ->
(* check RTE on the array before accessing its block length and offset *)
let env = !translate_rte_ref kf env array in
(* helper function *)
diff --git a/src/plugins/reduc/collect.ml b/src/plugins/reduc/collect.ml
index 448af313ea283befccaa4f5f45e872f423153a86..f71af89a6af656be9cd41bad7edc483692081403 100644
--- a/src/plugins/reduc/collect.ml
+++ b/src/plugins/reduc/collect.ml
@@ -85,7 +85,7 @@ let rec collect_off typ =
| TArray (arrtyp, e_opt, _) ->
debug "Array of length %a" (Pretty_utils.pp_opt Printer.pp_exp) e_opt;
begin try collect_array arrtyp [] (Cil.lenOfArray64 e_opt)
- with Cil.LenOfArray -> [] end
+ with Cil.LenOfArray _ -> [] end
| TVoid _ | TFun _ | TPtr _ | TEnum _ | TNamed _ | TBuiltin_va_list _
| TComp ({cfields = None}, _)-> []
diff --git a/src/plugins/value/domains/cvalue/cvalue_init.ml b/src/plugins/value/domains/cvalue/cvalue_init.ml
index d6cecc8bb7e738f2d54184f7b805db51b2998ddf..4faee93725faf82ad6fc7c6ee1cf5f88ca332381 100644
--- a/src/plugins/value/domains/cvalue/cvalue_init.ml
+++ b/src/plugins/value/domains/cvalue/cvalue_init.ml
@@ -287,9 +287,10 @@ let initialize_var_using_type varinfo state =
end;
!state
with
- | Cil.LenOfArray ->
+ | Cil.LenOfArray cause ->
Value_parameters.result ~once:true ~current:true
- "no size specified for array, assuming 0";
+ "problem with array size (%a), assuming 0"
+ Cil.pp_incorrect_array_length cause;
(* This is either a flexible array member (for which Cil
implicitly returns a size of 0, so we are doing the proper
thing), or an incomplete array (which is forbidden) *)
diff --git a/src/plugins/value/engine/evaluation.ml b/src/plugins/value/engine/evaluation.ml
index 9a171581a4fc9e7865ee0433a1c36c778d9c2ef7..5cc270b5bac32da4c1bb76cc7366f35bf64f4d64 100644
--- a/src/plugins/value/engine/evaluation.ml
+++ b/src/plugins/value/engine/evaluation.ml
@@ -1056,7 +1056,7 @@ module Make
let size_expr = Option.get array_size in (* array_size exists *)
assume_valid_index ~size ~size_expr ~index_expr index
with
- | Cil.LenOfArray -> `Value index, Alarmset.none (* unknown array size *)
+ | Cil.LenOfArray _ -> `Value index, Alarmset.none (* unknown array size *)
in
valid_index >>=: fun index ->
Loc.forward_index typ_pointed index roffset, typ_offs,
diff --git a/src/plugins/value/utils/widen.ml b/src/plugins/value/utils/widen.ml
index c2c63c2dff907c792e9efb14e3a2de9d65ff1dea..75db51158ff54761db2c5f4a34ccd7a5d75230f6 100644
--- a/src/plugins/value/utils/widen.ml
+++ b/src/plugins/value/utils/widen.ml
@@ -295,7 +295,7 @@ class pragma_widen_visitor init_widen_hints init_enclosing_loops = object(self)
let size = Cil.lenOfArray64 size in
if Integer.(gt size zero) then
self#add_index_hints size idx
- with Cil.LenOfArray -> ()
+ with Cil.LenOfArray _ -> ()
end
| _ -> ()
end
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..b4a00ef7aed6589641454c16903b943c79833606 100644
--- a/tests/syntax/oracle/very_large_integers.4.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.4.res.oracle
@@ -1,6 +1,6 @@
[kernel] Parsing very_large_integers.c (with preprocessing)
-[kernel] very_large_integers.c:50: Failure:
- Array length 9999999999999999999U is not a compile-time constant: no explicit initializer allowed.
+[kernel] very_large_integers.c:52: 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.
[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 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
diff --git a/tests/value/oracle/extern.res.oracle b/tests/value/oracle/extern.res.oracle
index 731cb592c363661e2c02429596b4a0254c5b429c..7fd64be0b6058acc2788224f41da4790c85d8988 100644
--- a/tests/value/oracle/extern.res.oracle
+++ b/tests/value/oracle/extern.res.oracle
@@ -7,7 +7,8 @@
[eva:unknown-size] extern.i:7: Warning:
during initialization of variable 'T4', size of type 'int const []' cannot be
computed (Size of array without number of elements.)
-[eva] extern.i:16: no size specified for array, assuming 0
+[eva] extern.i:16:
+ problem with array size (not a compile-time constant), assuming 0
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
T1 ∈ [--..--]