Actions
Bug #9560
closedFrama-C (CIL) does not support initialization of wide character arrays with wide character literals like GCC
Start date:
03/21/2019
Due date:
% Done:
0%
Estimated time:
Detected in build:
svn
Platform:
Published in build:
Description
For the attached file GCC 7 provides no warnings and errors with the following command (Linux x86_64):
gcc -Wall -fsyntax-only -fshort-wchar wchar.c
The corresponding command with Frama-C (CIL):
toplevel.opt -no-autoload-plugins -no-findlib -machdep gcc_x86_64 -c11 -remove-unused-inline-functions -remove-unused-static-functions -no-annot -keep-logical-operators -aggressive-merging -print -print-lines -no-print-annot -ocode cil.i wchar.c
terminates with errors:
[kernel] Parsing wchar.c (with preprocessing) [kernel] wchar.c:3:0: Failure: Using a wide string literal to initialize something other than a wchar_t array [kernel] User Error: skipping file wchar.c that has errors. [kernel] Frama-C aborted: invalid user input.
BTW, removing declaration of wchar_t results in strange syntax error. So, it is unclear how Frama-C (CIL) supports wide character arrays initialization.
Files
Actions