From 66fdfc2f70655faac9e88afd333293ee2de0abf5 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Thu, 25 Jan 2024 18:01:11 +0100
Subject: [PATCH] [kernel] Better localization for array length errors
---
src/kernel_internals/typing/cabs2cil.ml | 1 +
tests/syntax/oracle/very_large_integers.14.res.oracle | 2 +-
tests/syntax/oracle/very_large_integers.4.res.oracle | 2 +-
3 files changed, 3 insertions(+), 2 deletions(-)
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 3925038637d..16f71399f19 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -3364,6 +3364,7 @@ let integerArrayLength (leno: exp option) : int =
try lenOfArray leno
with
| LenOfArray cause ->
+ Cil.CurrentLoc.set len.eloc;
abort_context
"Array length %a is %a: no explicit initializer allowed."
Cil_printer.pp_exp len Cil.pp_incorrect_array_length cause
diff --git a/tests/syntax/oracle/very_large_integers.14.res.oracle b/tests/syntax/oracle/very_large_integers.14.res.oracle
index 7cbdaf67c3b..5846557a229 100644
--- a/tests/syntax/oracle/very_large_integers.14.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.14.res.oracle
@@ -4,7 +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:107: User Error: 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 77a8b542245..f30af367582 100644
--- a/tests/syntax/oracle/very_large_integers.4.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.4.res.oracle
@@ -5,7 +5,7 @@
60
61 #ifdef INIT_DESIGNATOR
62 int arr2[9999999999999999999U] = { [9999999999999999999U] = 42 };
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ ^^^^^^^^^^^^^^^^^^^^
63 #endif
64
[kernel] Frama-C aborted: invalid user input.
--
GitLab