From 94fffaf79b3b729cf97b0dfef2d21590413b9aea Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Mon, 19 Feb 2024 16:18:05 +0100
Subject: [PATCH] [kernel] more explicit error msg
---
src/kernel_internals/typing/cabs2cil.ml | 5 ++++-
tests/value/oracle/empty_base.1.res.oracle | 9 ++++++---
2 files changed, 10 insertions(+), 4 deletions(-)
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 6c8a903e494..c450ee61cfc 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -4822,7 +4822,10 @@ and doType (ghost:bool) isFuncArg
"Array length is too large.";
with
| SizeOfError (msg,_) ->
- Kernel.error ~once:true ~current:true "%s" 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
diff --git a/tests/value/oracle/empty_base.1.res.oracle b/tests/value/oracle/empty_base.1.res.oracle
index 43a088f4f72..bba69f8432c 100644
--- a/tests/value/oracle/empty_base.1.res.oracle
+++ b/tests/value/oracle/empty_base.1.res.oracle
@@ -1,11 +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: empty struct 'struct empty'
+[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: empty struct 'struct empty'
-[kernel] empty_base.c:50: User Error: empty struct 'struct empty'
+[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];
--
GitLab