Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Problems with value analysis

Hello,

Virgile Prevosto a ?crit :
> Le lun. 14 d?c. 2009 15:55:09 CET,
> "Hollas Boris (CR/AEY1)" <Boris.Hollas at de.bosch.com> a ?crit :
> 
>> - function set is invoked by set( &Ctx, -1, 0 ) in main(), which causes an out of bound access in set(). This is reported for the location in set(), where the out of bound accesss actually happens, but where it is not caused. How can the user discover the origin of the bug?
> 
> I have to admit that there is currently no easy to do it (note however
> that the value analysis itself can not decide by itself where the bug
> really is. It might have been better at spotting that the pre-condition
> of set was not fulfilled, though). However, value analysis gives an
> overview of the call stack each time it enters a function, such as
> 
> [value] computing for function set <-main.
>         Called from file.c:26.
> 
> (if you're using the gui, it is available in the console tab at the
> bottom of the window). This is quite helpful for following the flow of
> the program.
> In your case, since we're dealing with a true alarm which is
> always happening and causes an abrupt termination of the whole
> analysis, there's an additional possibility, and it goes with the
> answers to your second question:

Just my 2 cents in addition to the Virgile's answer...

Discovering the origin of the bug is mostly an human process, but some 
Frama-C plug-ins like Datascope and Slicing can help you a little bit 
via the Frama-C GUI. The first one shows you the statement that may 
contribute to the erroneous value (here the occurrence of 'idx' at line 
16). The second one can display the line of code which may contribute to 
the error.

I illustrate the use of the slicing on your small example.
- run "frama-c-gui -val foo.c" on your example
- right click on the buggy statement and select "Slicing"
- right click again on the same statement, select "Slicing", then "Slice 
lval"
- enter "idx" in the dialog box (why idx? because the assertion 
generated by the value analysis tells you that idx should belong to 
[0;100], while you can see that its value is -1 by clicking on 'idx' at 
the buggy statement: a wrong value for idx is the origin of the out of 
bound access)
- the green code is the only one which may contribute to the out of 
bound access

Hope this helps,
Julien