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] Use of Jessie and Value Analysis plug-in

Hello, Rovedy.


> Value Analysis 2) the entry point was the main function of the task
> and its body is showed below. When I executed the analysis, the
> plug-in shows the message below.  How I can treat this case?
>
> void main(void)
> {...
> while(FOREVER){
>        ?.
>     } /* END OF While FOREVER */
> }
>
> [value] Values for function main:
>          NON TERMINATING FUNCTION
>

There is no problem. The message telling you that main() doesn't
terminate is not a warning. Function main() does not terminate.
You can still observe values in the GUI (see for instance
http://blog.frama-c.com/index.php?post/2011/06/06/Fixing-robots%2C-part-1 )
or with Frama_C_show_each_...() and
Frama_C_dump_each() primitive calls (see section 8.3 in
http://frama-c.com/download/frama-c-value-analysis.pdf ).

Value Analysis 3) for refining my analysis, I tried the option
> ?slevel. The while (cited above) statement must be executed 3000
> cycles (I am considering only a part of a task). There is a for
> statement with 61 interactions. The correct choice must be 3000?
>

If you want everything to be unrolled completely, probably much
more than 3000, as I hope that the paragraph starting with
"The number n to use depends on the nature of the control ?ow
graph of the function to analyze" page 56 of the manual makes clear.
However, you should accept that it's not going to be possible to
unroll completely everything and start picking what is important,
using options like -slevel-function (perhaps introduced in Carbon),
and -no-results-function. It's an iterative process where you use
the information already computed to take decisions about what options
and annotations to use next. See for instance the Skein tutorial
(in the manual and continuing at http://blog.frama-c.com/index.php?tag/skein),
or the QuickLZ tutorial ( http://blog.frama-c.com/index.php?tag/QuickLZ ).

Value Analysis 4) is much appropriate to do the analysis with an
> individual function, providing a main function for each one with the
> initial values? In my experiment, I start with the main function of
> the task and I was added the function incrementally. I analyzed the
> final result. I noticed that when I executed the functions together a
> lot of alarms disappear if compared with an analysis with an
> individual function.
>

Analyzing individual functions is only interesting if you already
know what they are supposed to do, and you will still need to
tweak the initial context (because pointers are used for too many
different things in C).

Value Analysis 5) what to do with functions that access the hardware
> board? And the RTOS functions (for example, taskdelay - delay a task
> from executing)?
>

C implementations that give a reasonable approximation of the
intended behavior must be provided for these. You may want to
use functions listed in section 8.2.1 of the manual to implement
them. For instance, reading from a sensor may be replaced with
a Frama_C_interval() call.

General question) I used the Boron version. Is there a Carbon version
> for Windows?
>

The binary version for Windows of Frama-C Carbon is too large to be made
available. Is Windows the only OS you have? Carbon is available
in Debian Testing and there is a binary package for Mac OS X on
the website.

Pascal
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20110819/8743de36/attachment.htm>