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