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 new file mode 100644 index 0000000000000000000000000000000000000000..1891c5ad9463650874073250229a53f597c793b9 --- /dev/null +++ b/tests/syntax/init_array_string.i @@ -0,0 +1,19 @@ +char* ptr = "A" "B"; + +char* ptr2 = ("A" "B"); + +char a[] = "A" "B"; + +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 new file mode 100644 index 0000000000000000000000000000000000000000..e678a6a4f019ddd943735f165c78b75040a1f6eb --- /dev/null +++ b/tests/syntax/oracle/init_array_string.res.oracle @@ -0,0 +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'}}; +