diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 734680610c0fdb7ab6044b46f411a7816e4f6070..c450ee61cfc48a5d7869de93ab8551f277659f61 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -4794,9 +4794,41 @@ and doType (ghost:bool) isFuncArg
let cst = constFold true len' in
(match cst.enode with
| Const(CInt64(i, _, _)) ->
- if Integer.lt i Integer.zero then
- Kernel.error ~once:true ~current:true
- "Array length is negative."
+ begin
+ if Integer.lt i Integer.zero then
+ Kernel.error ~once:true ~current:true
+ "Array length is negative."
+ else
+ (* Check if array size (nb elem * size elem) is smaller than
+ max size. *)
+ try
+ let elem_size =
+ if Cil.isCompleteType bt &&
+ not (Cil.is_variably_modified_type bt)
+ then
+ Integer.of_int @@ bytesSizeOf bt
+ else
+ (* Incomplete types can't be array elements,
+ and multi-dimensional VLAs are currently unsupported.
+ In both cases an error has already been raised,
+ we just check here that the size is not widely off.*)
+ Integer.one
+ in
+ let size_t = bitsSizeOfInt theMachine.kindOfSizeOf in
+ let size_max = Cil.max_unsigned_number size_t in
+ let array_size = Integer.mul i elem_size in
+ if Integer.gt array_size size_max then
+ Kernel.error ~once:true ~current:true
+ "Array length is too large.";
+ with
+ | SizeOfError (msg,_) ->
+ Kernel.error ~once:true ~current:true
+ "Unable to compute the size of array element '%a': %s"
+ Cil_printer.pp_typ bt
+ msg
+ | Invalid_argument msg ->
+ Kernel.fatal ~current:true "%s" msg
+ end
| _ when not allowVarSizeArrays ->
if isConstant cst then
(* e.g., there may be a float constant involved.
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 5d7b28b0c82a97af448d5b6e7c1e8c392ddb34cd..eb576984e72b2524b3a4ad6375d8c5344a1e9678 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -4510,7 +4510,7 @@ and bytesSizeOf t = (bitsSizeOf t) lsr 3
and sizeOf ~loc t =
try
- integer ~loc ((bitsSizeOf t) lsr 3)
+ integer ~loc (bytesSizeOf t)
with SizeOfError _ -> new_exp ~loc (SizeOf(t))
and fieldBitsOffset (f : fieldinfo) : int * int =
@@ -4611,14 +4611,13 @@ and constFold (machdep: bool) (e: exp) : exp =
| Const(CChr c) -> new_exp ~loc (Const(charConstToIntConstant c))
| Const(CEnum {eival = v}) -> constFold machdep v
| Const (CReal _ | CWStr _ | CStr _ | CInt64 _) -> e (* a constant *)
- | SizeOf t when machdep -> begin
- try
- let bs = bitsSizeOf t in
- kinteger ~loc theMachine.kindOfSizeOf (bs / 8)
+ | SizeOf t when machdep ->
+ begin
+ try kinteger ~loc theMachine.kindOfSizeOf (bytesSizeOf t)
with SizeOfError _ -> e
end
- | SizeOfE e when machdep -> constFold machdep
- (new_exp ~loc:e.eloc (SizeOf (typeOf e)))
+ | SizeOfE e when machdep ->
+ constFold machdep (new_exp ~loc:e.eloc (SizeOf (typeOf e)))
| SizeOfStr s when machdep ->
kinteger ~loc theMachine.kindOfSizeOf (1 + String.length s)
| AlignOf t when machdep ->
diff --git a/src/plugins/wp/tests/wp_plugin/bigarray.c b/src/plugins/wp/tests/wp_plugin/bigarray.c
index 96637a1809758f92a16512c00adad0065276dfa6..f243f5d0f68bcf5f98019c8c870e84d1aa16a41c 100644
--- a/src/plugins/wp/tests/wp_plugin/bigarray.c
+++ b/src/plugins/wp/tests/wp_plugin/bigarray.c
@@ -1,21 +1,10 @@
-/* run.config
- EXIT: 0
- OPT: -cpp-extra-args="-DFIT"
- EXIT: 1
- OPT: -cpp-extra-args="-DLARGE"
- */
-
/* run.config_qualif
DONTRUN:
*/
#include <stdint.h>
-#ifdef FIT
+
#define SIZE (SIZE_MAX / sizeof(int))
-#endif
-#ifdef LARGE
-#define SIZE SIZE_MAX
-#endif
/*@
assigns \result \from p[0..n-1];
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/bigarray.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/bigarray.1.res.oracle
deleted file mode 100644
index 41201e6e8348610aac541642ec2b5993b45413e1..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_plugin/oracle/bigarray.1.res.oracle
+++ /dev/null
@@ -1,12 +0,0 @@
-# frama-c -wp [...]
-[kernel] Parsing bigarray.c (with preprocessing)
-[kernel] bigarray.c:30: Warning:
- Cannot represent length of array as an attribute
-[wp] Running WP plugin...
-[wp] [Valid] Goal f_exits (Cfg) (Unreachable)
-[wp] [Valid] Goal f_terminates (Cfg) (Trivial)
-[wp] Warning: Missing RTE guards
-[wp] bigarray.c:30: Warning: Array size too large (0xFFFFFFFFFFFFFFFF)
-[wp] bigarray.c:31: Warning: Array size too large (0xFFFFFFFFFFFFFFFF)
-[wp] bigarray.c:21: User Error: Array size too large (0xFFFFFFFFFFFFFFFF)
-[kernel] Plug-in wp aborted: invalid user input.
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/bigarray.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/bigarray.res.oracle
similarity index 75%
rename from src/plugins/wp/tests/wp_plugin/oracle/bigarray.0.res.oracle
rename to src/plugins/wp/tests/wp_plugin/oracle/bigarray.res.oracle
index d0aae4c8e069ee7f92b2b1db3d91bd19be7c80d7..edc3c3e8bd788ed5f4a240d6366891a8482ce2e2 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/bigarray.0.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/bigarray.res.oracle
@@ -1,6 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing bigarray.c (with preprocessing)
-[kernel] bigarray.c:30: Warning:
+[kernel] bigarray.c:19: Warning:
Cannot represent length of array as an attribute
[wp] Running WP plugin...
[wp] [Valid] Goal f_exits (Cfg) (Unreachable)
@@ -10,23 +10,23 @@
Function f
------------------------------------------------------------
-Goal Loop assigns (file bigarray.c, line 27):
+Goal Loop assigns (file bigarray.c, line 16):
Prove: true.
------------------------------------------------------------
Goal Assigns nothing in 'f':
-Effect at line 30
+Effect at line 19
Prove: true.
------------------------------------------------------------
-Goal Decreasing of Loop variant at loop (file bigarray.c, line 30):
+Goal Decreasing of Loop variant at loop (file bigarray.c, line 19):
Prove: true.
------------------------------------------------------------
-Goal Positivity of Loop variant at loop (file bigarray.c, line 30):
+Goal Positivity of Loop variant at loop (file bigarray.c, line 19):
Prove: true.
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_typed/oracle/too_large_array.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/too_large_array.0.res.oracle
deleted file mode 100644
index 7185f12777a04c6c3fb349320214af3da92c505a..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_typed/oracle/too_large_array.0.res.oracle
+++ /dev/null
@@ -1,12 +0,0 @@
-# frama-c -wp [...]
-[kernel] Parsing too_large_array.i (no preprocessing)
-[kernel] too_large_array.i:12: Warning:
- Cannot represent length of array as an attribute
-[wp] Running WP plugin...
-[wp] [Valid] Goal merge_exits (Cfg) (Unreachable)
-[wp] Warning: Missing RTE guards
-[wp] too_large_array.i:13: Warning: Array size too large (0xFFFFFFFFFFFFFFFF)
-[wp] too_large_array.i:14: Warning:
- Missing assigns clause (assigns 'everything' instead)
-[wp] too_large_array.i:11: User Error: Array size too large (0xFFFFFFFFFFFFFFFF)
-[kernel] Plug-in wp aborted: invalid user input.
diff --git a/src/plugins/wp/tests/wp_typed/oracle/too_large_array.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/too_large_array.1.res.oracle
deleted file mode 100644
index 9d95ea7570c68ed69fbb86d77f665ba8fa95ce38..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_typed/oracle/too_large_array.1.res.oracle
+++ /dev/null
@@ -1,12 +0,0 @@
-# frama-c -wp -wp-model 'Typed (Ref)' [...]
-[kernel] Parsing too_large_array.i (no preprocessing)
-[kernel] too_large_array.i:12: Warning:
- Cannot represent length of array as an attribute
-[wp] Running WP plugin...
-[wp] [Valid] Goal merge_exits (Cfg) (Unreachable)
-[wp] Warning: Missing RTE guards
-[wp] too_large_array.i:13: Warning: Array size too large (0xFFFFFFFFFFFFFFFF)
-[wp] too_large_array.i:14: Warning:
- Missing assigns clause (assigns 'everything' instead)
-[wp] too_large_array.i:11: User Error: Array size too large (0xFFFFFFFFFFFFFFFF)
-[kernel] Plug-in wp aborted: invalid user input.
diff --git a/tests/syntax/oracle/too_large_array.res.oracle b/tests/syntax/oracle/too_large_array.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..1db88ceff98a128c833f34e29b0639593793b8a8
--- /dev/null
+++ b/tests/syntax/oracle/too_large_array.res.oracle
@@ -0,0 +1,6 @@
+[kernel] Parsing too_large_array.i (no preprocessing)
+[kernel] too_large_array.i:12: User Error: Array length is too large.
+[kernel] too_large_array.i:12: Warning:
+ Cannot represent length of array as an attribute
+[kernel] User Error: stopping on file "too_large_array.i" that has errors.
+[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/very_large_integers.1.res.oracle b/tests/syntax/oracle/very_large_integers.1.res.oracle
index 4f4479d850994060abd17b9c1bb2c03213580381..543e2f77a34315e860d772c2f77dff770b5c85e6 100644
--- a/tests/syntax/oracle/very_large_integers.1.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.1.res.oracle
@@ -1,4 +1,5 @@
[kernel] Parsing very_large_integers.c (with preprocessing)
+[kernel] very_large_integers.c:41: User Error: Array length is too large.
[kernel] very_large_integers.c:42: User Error:
Cannot represent the integer 99999999999999999999U
[kernel] very_large_integers.c:42: User Error:
diff --git a/tests/syntax/oracle/very_large_integers.14.res.oracle b/tests/syntax/oracle/very_large_integers.14.res.oracle
index 258dd40268376ba56fbcb9483b044db1419715b2..bfd5d8b7eb57423236a1136fb001b9e59c49351b 100644
--- a/tests/syntax/oracle/very_large_integers.14.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.14.res.oracle
@@ -4,6 +4,7 @@
[kernel] very_large_integers.c:84: Warning:
ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
(9223372036854775808) )
+[kernel] very_large_integers.c:106: User Error: Array length is too large.
[kernel] very_large_integers.c:113: User Error:
array length too large: 7205759403792794
111 };
diff --git a/tests/syntax/oracle/very_large_integers.4.res.oracle b/tests/syntax/oracle/very_large_integers.4.res.oracle
index ca9b712f16e76c21ccb54af94f7894a05433dd92..77a8b542245f0fbe7d3a2607a9f110cf9a092df9 100644
--- a/tests/syntax/oracle/very_large_integers.4.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.4.res.oracle
@@ -1,4 +1,5 @@
[kernel] Parsing very_large_integers.c (with preprocessing)
+[kernel] very_large_integers.c:62: User Error: Array length is too large.
[kernel] very_large_integers.c:62: User Error:
Array length 9999999999999999999U is too big: no explicit initializer allowed.
60
diff --git a/src/plugins/wp/tests/wp_typed/too_large_array.i b/tests/syntax/too_large_array.i
similarity index 100%
rename from src/plugins/wp/tests/wp_typed/too_large_array.i
rename to tests/syntax/too_large_array.i
diff --git a/tests/value/oracle/empty_base.1.res.oracle b/tests/value/oracle/empty_base.1.res.oracle
index eb0f8ece4e0737806ec80e0a2bea560d2eddb641..bba69f8432c7a4c311b70f979773601645d4e353 100644
--- a/tests/value/oracle/empty_base.1.res.oracle
+++ b/tests/value/oracle/empty_base.1.res.oracle
@@ -1,8 +1,14 @@
[kernel] Parsing empty_base.c (with preprocessing)
[kernel] empty_base.c:13: User Error:
empty structs only allowed for GCC/MSVC machdeps; see option -machdep or run 'frama-c -machdep help' for the list of available machdeps
+[kernel] empty_base.c:48: User Error:
+ Unable to compute the size of array element 'struct empty': empty struct 'struct empty'
[kernel] empty_base.c:48: User Error:
zero-length arrays only allowed for GCC/MSVC machdeps; see option -machdep or run 'frama-c -machdep help' for the list of available machdeps
+[kernel] empty_base.c:49: User Error:
+ Unable to compute the size of array element 'struct empty': empty struct 'struct empty'
+[kernel] empty_base.c:50: User Error:
+ Unable to compute the size of array element 'struct empty': empty struct 'struct empty'
[kernel] empty_base.c:50: User Error:
empty initializers only allowed for GCC/MSVC machdeps; see option -machdep or run 'frama-c -machdep help' for the list of available machdeps
48 struct empty empty_array_of_empty[0];