diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 4bac9159e132e1c85e3566fd91ffe02eb70ae498..471bf33f62c10109b6778b760901dc5eb19a9dc3 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -4827,7 +4827,8 @@ and doType (ghost:bool) isFuncArg
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
+ Kernel.warning ~wkey:Kernel.wkey_large_array
+ ~once:true ~current:true
"Array length is too large.";
with
| SizeOfError (msg,_) ->
diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml
index 5d6bddf2a120cc5c4f089f1feee67332c71aa67c..a347a92f2d5350e0d7906a5edf2c1f0e0937e627 100644
--- a/src/kernel_services/plugin_entry_points/kernel.ml
+++ b/src/kernel_services/plugin_entry_points/kernel.ml
@@ -157,6 +157,9 @@ let () = set_warn_status wkey_ghost_bad_use Log.Werror
let wkey_acsl_float_compare = register_warn_category "acsl-float-compare"
let () = set_warn_status wkey_acsl_float_compare Log.Winactive
+let wkey_large_array = register_warn_category "too-large-array"
+let () = set_warn_status wkey_large_array Log.Werror
+
let wkey_conditional_feature =
register_warn_category "parser:conditional-feature"
diff --git a/src/kernel_services/plugin_entry_points/kernel.mli b/src/kernel_services/plugin_entry_points/kernel.mli
index 314dbbdc1d9d10f9b0bfbf019391c3fb11a00227..20f4c1bf06c0742c567e6130e5f34f923a0f8f6c 100644
--- a/src/kernel_services/plugin_entry_points/kernel.mli
+++ b/src/kernel_services/plugin_entry_points/kernel.mli
@@ -162,6 +162,8 @@ val wkey_ghost_bad_use: warn_category
val wkey_acsl_float_compare: warn_category
+val wkey_large_array: warn_category
+
val wkey_conditional_feature: warn_category
(** parsing feature that is only supported in specific modes
(e.g. C11, gcc, ...). *)
diff --git a/tests/misc/oracle/audit-out.json b/tests/misc/oracle/audit-out.json
index ae58cd00a3b50374e3af74c1d047f56f40b67d21..da80b2ca65374be357e44b1ca62fea739281239a 100644
--- a/tests/misc/oracle/audit-out.json
+++ b/tests/misc/oracle/audit-out.json
@@ -63,7 +63,7 @@
"parser:conditional-feature", "parser:unnamed-typedef",
"parser:unsupported", "parser:unsupported:attributes",
"plugin-not-loaded", "pp", "pp:compilation-db", "pp:line-directive",
- "typing", "typing:implicit-conv-void-ptr",
+ "too-large-array", "typing", "typing:implicit-conv-void-ptr",
"typing:implicit-function-declaration",
"typing:incompatible-pointer-types",
"typing:incompatible-types-call", "typing:inconsistent-specifier",
diff --git a/tests/syntax/oracle/too_large_array.res.oracle b/tests/syntax/oracle/too_large_array.res.oracle
index 1db88ceff98a128c833f34e29b0639593793b8a8..c5df2b706f22b915013c35ed485c5bfbcc44301b 100644
--- a/tests/syntax/oracle/too_large_array.res.oracle
+++ b/tests/syntax/oracle/too_large_array.res.oracle
@@ -1,6 +1,7 @@
[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] too_large_array.i:12: Warning:
+ 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] Warning: warning too-large-array treated as deferred error. See above messages for more information.
[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 2a1bce76081fd479209be6cb1e51193270f0fce5..4e44ad885e4bd997af03b0e734d21cbbadbc594a 100644
--- a/tests/syntax/oracle/very_large_integers.1.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.1.res.oracle
@@ -1,5 +1,6 @@
[kernel] Parsing very_large_integers.c (with preprocessing)
-[kernel] very_large_integers.c:41: User Error: Array length is too large.
+[kernel:too-large-array] very_large_integers.c:41: Warning:
+ 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 acee0c62d23cdcd3a31efe64314cb577c50d4c19..66a2c5ad36e0111b7b8f36217dee37aa6418d678 100644
--- a/tests/syntax/oracle/very_large_integers.14.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.14.res.oracle
@@ -4,7 +4,8 @@
[kernel] very_large_integers.c:87: Warning:
ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
(9223372036854775808) )
-[kernel] very_large_integers.c:107: User Error: Array length is too large.
+[kernel:too-large-array] very_large_integers.c:107: Warning:
+ Array length is too large.
[kernel] very_large_integers.c:114: User Error:
array length too large: 7205759403792794
112 // Previously caused Out of memory
diff --git a/tests/syntax/oracle/very_large_integers.4.res.oracle b/tests/syntax/oracle/very_large_integers.4.res.oracle
index f30af367582a82c726be86d33ea3487afffee4a2..3ea7e8c28035e0af5790ae6fb0bd7ebaac144733 100644
--- a/tests/syntax/oracle/very_large_integers.4.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.4.res.oracle
@@ -1,5 +1,6 @@
[kernel] Parsing very_large_integers.c (with preprocessing)
-[kernel] very_large_integers.c:62: User Error: Array length is too large.
+[kernel:too-large-array] very_large_integers.c:62: Warning:
+ Array length is too large.
[kernel] very_large_integers.c:62: User Error:
Array length 9999999999999999999U is too big: no explicit initializer allowed.
60