--- layout: fc_discuss_archives title: Message 19 from Frama-C-discuss on August 2011 ---
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 >