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
Updated by Evgeny Novikov about 5 years ago
I revealed that Frama-C (CIL) likes just defined wchar_t and something like:
wchar_t *var = L"Hello";
In this way it supports type definitions based on wchar_t as well.
Thus it just does not support wide character arrays with or without specified sizes.
Updated by Mikhail Mandrykin about 5 years ago
Essentially the problem is that Frama-C (CIL) doesn't have an analogue of GCC's "-fshort-wchar
". This option controls the underlying type of the wchar literals (L""
). For now I added a new option -short-wchar
to simulate the behavior of "fshort-wchar
" (but it works not only with "-machdep gcc_x86_64
", but also other machdeps).
Updated by Evgeny Novikov about 5 years ago
- Status changed from New to Closed
With the new option Frama-C (CIL) does not fail on initialization of short wide character arrays.
Actions