diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml index 8bd77a0e771906eda26d66cda8b0d0e37a6b2386..a45a7cc00657e86cadf0ee28cd6300fcfb495dd4 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 b301c8d102c89b5af92f735919eba4354067c9b4..1891c5ad9463650874073250229a53f597c793b9 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 92a54fcd30d30a8e538a08cdce4cbe65e3a9caa8..e678a6a4f019ddd943735f165c78b75040a1f6eb 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'}};