From e7b80bd16cad72aa8d96633b1dc0fe9f77696473 Mon Sep 17 00:00:00 2001
From: Alexandre DOYEN <alexandre.doyen@cea.fr>
Date: Tue, 16 Apr 2024 16:52:47 +0200
Subject: [PATCH] Correctif pour le ticket #1343
---
src/kernel_internals/typing/cabs2cil.ml | 10 +++-------
1 file changed, 3 insertions(+), 7 deletions(-)
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 471bf33f62c..bebdb18ed93 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -3042,9 +3042,8 @@ let rec collectInitializer
| Some ni when Integer.ge ni Integer.zero -> to_integer ni, false
| _ ->
abort_context
- "Array length %a is not a compile-time constant: \
- no explicit initializer allowed."
- Cil_printer.pp_exp len
+ "\"Variable length array in structure\" extension is not supported"
+ len
end
| _ ->
(* unsized array case, length comes from initializers *)
@@ -4850,10 +4849,7 @@ and doType (ghost:bool) isFuncArg
Cil_printer.pp_exp cst
else
Kernel.error ~once:true ~current:true
- "Array length %a is not a compile-time constant,@ \
- and currently VLAs may only have their first dimension \
- as variable."
- Cil_printer.pp_exp cst
+ "\"Variable length array in structure\" extension is not supported"
| _ -> ());
if Cil.isZero len' && not allowZeroSizeArrays &&
not (Cil.gccMode () || Cil.msvcMode ())
--
GitLab