Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000593Frama-CKernelpublic2010-09-30 14:062010-10-01 10:11
Assigned Tovirgile 
PlatformOSOS Version
Product Version 
Target VersionFixed in Version 
Summary0000593: Parse error when using a wide string literal to initialize uint16 array
DescriptionI'm trying to analyze Brew with Frama-C. OS - windows XP. I've created simple Brew project(see attach), preprocessed it with Visual Studio and after it try to analyze with Frama-C: C:\Frama-C\bin>frama-c.exe "\Program Files\BREW 3.1.5\sdk\examples\helloworld"\*.i Also, I've tried to add files to project, using user interface, but nothing happened.
TagsNo tags attached.
Attached Fileszip file icon [^] (22,414 bytes) 2010-09-30 14:06

- Relationships

-  Notes
pascal (reporter)
2010-09-30 15:15

I have reproduced the bug. Typing "frama-c helloworld.i", I get the error message: .\\helloworld.c:209:[kernel] failure: Using a wide string literal to initialize something other than a wchar_t array The line is: AECHAR text[10] = L"0.0"; where AECHAR is a typedef: typedef uint16 AECHAR; One possible continuation is to comment the line AECHAR text[10] = L"0.0"; in the .i file (the variable text is not used anyway). If you do that, you can continue the analysis for instance with the command: frama-c-gui helloworld.i -lib-entry -main HelloWorld_HandleEvent -val This does not produce very interesting results because too many functions are missing. If you want static analysis that works in these conditions in order to find obvious bugs, we recommend Clang ( ).
Maria (reporter)
2010-10-01 09:07

I know, that problem is in this string(AECHAR text[10] = L"0.0";), I've added it to show error. Problem is that my real project has lots of that kind of strings(I can't comment them all). Does this mean that this error is "Work as designed" feature? Anyway, thanks for advise, I'll try Clang.
pascal (reporter)
2010-10-01 10:08

We recognize that failing to parse the definition of text[10] is a bug or at least that parsing it is a desirable feature. We will look at the difficulty of supporting it and if it does not seem too complicated, we will change the parser. This is the meaning of the "Confirmed" status of this bug report. Because we anticipate that the next step in your usage of Frama-C will disappoint you anyway, we will not do it urgently, though. If you want to produce useful results with Frama-C, you must either: - using the value analysis, include in the analysis project the source code of the functions that are part of the SDK. This will make the project big, but the value analysis does not work well when the source code of some functions is missing. - using Jessie for modular verification of only some functions, be ready to write ACSL specifications.
pascal (reporter)
2010-10-01 10:11

Here is a better link for the static analysis part of clang:

- Issue History
Date Modified Username Field Change
2010-09-30 14:06 Maria New Issue
2010-09-30 14:06 Maria File Added:
2010-09-30 15:15 pascal Note Added: 0001165
2010-09-30 15:15 pascal Assigned To => virgile
2010-09-30 15:15 pascal Status new => acknowledged
2010-09-30 21:49 pascal Summary can't analyze project => Parse error when using a wide string literal to initialize uint16 array
2010-09-30 21:49 pascal Description Updated
2010-10-01 09:07 Maria Note Added: 0001166
2010-10-01 10:08 pascal Note Added: 0001167
2010-10-01 10:08 pascal Status acknowledged => confirmed
2010-10-01 10:11 pascal Note Added: 0001168

Copyright © 2000 - 2020 MantisBT Team
Powered by Mantis Bugtracker