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 Boris,

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:
> 
> - Non termination is reported for functions set() and main(). As there are no loops in set(), is this message a bug or just a false positive?
> 

Neither. This is somehow related to Q2 in the FAQ of the value analysis
manual
http://frama-c.cea.fr/download/value-analysis-Beryllium-20090902.pdf

Value analysis has detected that an error will always occur
when dereferencing pCtx->buf[idx]. There is thus no possibility to go
further on this program path. Since this is the only one in function
set, it concludes that the call will never terminate normally[1]. This
state is handled back to the main function, where the set call is also
on the only possible path. Similarly, main will thus never return
normally. Hence the warning about non-termination (which should maybe
read "non-termination or abnormal termination" but this is a bit long).
In the gui, the code below the issue appears on a red background,
indicating that the code is dead: no normal execution will ever get
there. Hence, there is another way to trace back the origin of the
issue: start at the entry point of your analysis, and see if some dead
code appears in the middle of a block. Indeed, you can see some dead
code in other circumstances, e.g. with 

if (0) x=1;

x=1 is dead, but there is no issue. However, if you have 

*p=2; 
x=1;

with *p=2 considered alive and x=1 dead, it shows that p is invalid.
Similarly, with

f(x);
x=1;

and f(x) alive and x=1 dead, you know that the call to f was not
exactly successful. You can then go to the definition of f (go to
definition in contextual menu when selecting f[2]) and repeat the
operation if needed.

Hope this helps,
-- 
E tutto per oggi, a la prossima volta.
Virgile

[1] More precisely, you've invoked undefined behavior, but for the
purpose of value analysis it is easier to say that execution stops,
since anything is allowed by the norm to happen after that.
[2] When selecting the declaration of f, you can also go back
to the caller of f if needed.