--- layout: fc_discuss_archives title: Message 19 from Frama-C-discuss on August 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Use of Jessie and Value Analysis plug-in



Hello Pascal,

The explanation about Value analysis was very enlightening.
I will read the manual and links, and will try  some functions of Frama-C.

I will try to compile the Carbon version for Windows-Cygwin (Will I
get, won't I?)

I'm very grateful for the help.

Best regards,
Rovedy

2011/8/18 Pascal Cuoq <pascal.cuoq at gmail.com>:
> 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
>
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
>