From 8bc287d44964dbf170f88f6109ea4e8d271f7fed Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Mon, 10 Feb 2020 17:35:32 +0100
Subject: [PATCH] [kernel] Keep some reference to forbidden explicit
initializer.
---
src/kernel_internals/typing/cabs2cil.ml | 6 ++++--
1 file changed, 4 insertions(+), 2 deletions(-)
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index aa8deb6723c..385f2198dc8 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -3360,7 +3360,8 @@ let rec collectInitializer
(Integer.to_int ni), false
| _ ->
Kernel.fatal ~current:true
- "Array length %a is not a compile-time constant."
+ "Array length %a is not a compile-time constant: \
+ no explicit initializer allowed."
Cil_printer.pp_exp len
end
| _ ->
@@ -3678,7 +3679,8 @@ let integerArrayLength (leno: exp option) : int =
try lenOfArray leno
with LenOfArray ->
Kernel.fatal ~current:true
- "Array length %a is not a compile-time constant."
+ "Array length %a is not a compile-time constant: \
+ no explicit initializer allowed."
Cil_printer.pp_exp len
let find_field_offset cond (fidlist: fieldinfo list) : offset =
--
GitLab