diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml index 6c8a903e494455e6a9948001a05ccab2bb5f35cc..c450ee61cfc48a5d7869de93ab8551f277659f61 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 43a088f4f720c9a30218909ef60928752bb52c20..bba69f8432c7a4c311b70f979773601645d4e353 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];