Project

General

Profile

Actions
Copy link

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
Assignee:
Mikhail Mandrykin
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
Copy link

Also available in: Atom PDF