|Anonymous | Login | Signup for a new account||2019-07-21 22:20 CEST|
|Main | My View | View Issues | Change Log | Roadmap | Repositories|
|View Issue Details|
|ID||Project||Category||View Status||Date Submitted||Last Update|
|0000593||Frama-C||Kernel||public||2010-09-30 14:06||2010-10-01 10:11|
|Target Version||Fixed in Version|
|Summary||0000593: Parse error when using a wide string literal to initialize uint16 array|
|Description||I'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.
|Tags||No tags attached.|
|Attached Files||helloworld.zip [^] (22,414 bytes) 2010-09-30 14:06|
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 = L"0.0";
where AECHAR is a typedef:
typedef uint16 AECHAR;
One possible continuation is to comment the line AECHAR text = 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 (http://clang.llvm.org/ [^] ).
I know, that problem is in this string(AECHAR text = 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.
We recognize that failing to parse the definition of text 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.
Here is a better link for the static analysis part of clang:
|2010-09-30 14:06||Maria||New Issue|
|2010-09-30 14:06||Maria||File Added: helloworld.zip|
|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 - 2019 MantisBT Team|