Project

General

Profile

Actions

Bug #9560

closed

Frama-C (CIL) does not support initialization of wide character arrays with wide character literals like GCC

Added by Evgeny Novikov about 5 years ago. Updated about 5 years ago.

Status:
Closed
Priority:
Urgent
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

wchar.c (115 Bytes) wchar.c Evgeny Novikov, 03/21/2019 11:25 AM
Actions #1

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.

Actions #2

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).

Actions #3

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

Also available in: Atom PDF