From 6a0c34f658eddfea38798f3359136f84d9087cd8 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Wed, 10 Jul 2024 19:14:42 +0200
Subject: [PATCH] [typing] allow parenthesizing string literals that initialize
an array
---
src/kernel_internals/typing/cabs2cil.ml | 31 +++++++++++++------
tests/syntax/init_array_string.i | 8 +++++
.../oracle/init_array_string.res.oracle | 7 +++++
3 files changed, 36 insertions(+), 10 deletions(-)
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 8bd77a0e771..a45a7cc0065 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -7947,16 +7947,21 @@ and doInitializer loc local_env (vi: varinfo) (inite: Cabs.init_expression)
let open Current_loc.Operators in
let checkArrayInit ty init =
- if Cil.isArrayType ty then
- match init with
- | COMPOUND_INIT _
- | SINGLE_INIT
- { expr_node =
- CONSTANT (CONST_STRING _
- | CONST_WSTRING _)} -> ()
- | _ ->
- Kernel.error ~current:true ~once:true
- "Array initializer must be an initializer list or string literal"
+ let init_ok =
+ if Cil.isArrayType ty then
+ match init with
+ | COMPOUND_INIT _ -> true
+ | SINGLE_INIT e ->
+ (match stripParen e with
+ { expr_node =
+ CONSTANT (CONST_STRING _ | CONST_WSTRING _)} -> true
+ | _ -> false)
+ | _ -> false
+ else true
+ in
+ if not init_ok then
+ Kernel.error ~current:true ~once:true
+ "Array initializer must be an initializer list or string literal";
in
Kernel.debug ~dkey:Kernel.dkey_typing_init
"@\nStarting a new initializer for %s : %a@\n"
@@ -8005,6 +8010,12 @@ and doInitializer loc local_env (vi: varinfo) (inite: Cabs.init_expression)
and doInit local_env asconst preinit so acc initl =
let ghost = local_env.is_ghost in
let whoami fmt = Cil_printer.pp_lval fmt (Var so.host, so.soOff) in
+ let initl =
+ match initl with
+ | (initwhat, SINGLE_INIT e)::tl ->
+ (initwhat, SINGLE_INIT (stripParen e)) ::tl
+ | _ -> initl
+ in
let initl1 =
match initl with
| (Cabs.NEXT_INIT,
diff --git a/tests/syntax/init_array_string.i b/tests/syntax/init_array_string.i
index b301c8d102c..1891c5ad946 100644
--- a/tests/syntax/init_array_string.i
+++ b/tests/syntax/init_array_string.i
@@ -9,3 +9,11 @@ char b[] = ("A" "B");
char c[] = "ABC";
char d[] = ("ABC");
+
+struct S {
+ char c[42];
+};
+
+struct S s = { .c = ("foo") };
+
+char as[3][4] = { ("bar"), [2] = ("bla") };
diff --git a/tests/syntax/oracle/init_array_string.res.oracle b/tests/syntax/oracle/init_array_string.res.oracle
index 92a54fcd30d..e678a6a4f01 100644
--- a/tests/syntax/oracle/init_array_string.res.oracle
+++ b/tests/syntax/oracle/init_array_string.res.oracle
@@ -1,9 +1,16 @@
[kernel] Parsing init_array_string.i (no preprocessing)
/* Generated by Frama-C */
+struct S {
+ char c[42] ;
+};
char *ptr = (char *)"AB";
char *ptr2 = (char *)"AB";
char a[3] = {(char)'A', (char)'B', (char)'\000'};
char b[3] = {(char)'A', (char)'B', (char)'\000'};
char c[4] = {(char)'A', (char)'B', (char)'C', (char)'\000'};
char d[4] = {(char)'A', (char)'B', (char)'C', (char)'\000'};
+struct S s = {.c = {(char)'f', (char)'o', (char)'o', (char)'\000'}};
+char as[3][4] =
+ {{(char)'b', (char)'a', (char)'r', (char)'\000'},
+ [2] = {(char)'b', (char)'l', (char)'a', (char)'\000'}};
--
GitLab