--- layout: fc_discuss_archives title: Message 33 from Frama-C-discuss on October 2012 ---
Thank you so much for timely replying me. In honest, I like frama-c very much. It's so powerful. It is amazing that value analysis can be so precisely. I can almost do whatever I want by using this analysis framework. > You are using Frama-C's value analysis plug-in, a state-of-the-art static analysis > component that has been successfully applied to large codebases of industrial > embedded C code. Which industrial embedded C code has been successfully applied? Is there any large open source codebases have been analysis by using frama-c? > But wait! You are not doing a verification of Vim with Frama-C's value analysis. > You are using the value analysis in an unconventional fashion to obtain results > that you need for something else you want to do. > Would you say that a hammer is unable > to handle nails because you tried to smash it on a hundred nails at once and it > did not do what you expected? I'm sorry to use frama-c in a wrong way. Maybe I should first use CIL (C Intermediate Language) to merge all vim source codes into a single file. Then, use frama-c to analysis that merged file. At that situation, I have no need to set that '-main' option for each function and do value analysis only once. > > I have use the following options to speed up value analysis: > > 1. -slevel 10000 > > Do you have any reason to think that this makes the analysis faster? > I think that the documentation is rather clear on the fact that option -slevel > improves precision, usually at the cost of time and memory. > I just try this option for another time. It did not speed up the value analysis. I have read the documentation before. But when I use the command line: 'frama-c -value-help' It shows that: "... -slevel <n> use <n> as number of path to explore in parallel ..." This makes me misunderstanding and wrongly using this option. Thanks for remind me of this option. > > Is there any method to ignore those errors like "length of array size > > is zero" and continue to do value analysis? > > The C99 standard says: > > 6.7.5.2 Array declarators > Constraints > > 1. [...] If the expression is a constant expression, it shall have a value greater > than zero. > Thank you. Maybe the linux-kernel version which I analyzed is out of date. I would like to know if there is anybody have succeed analyzing Linux-kernel by using your group's tool frama-c before? I can just successfully saved all temp files of linux-kernel source code by change the makefile.build file. Ben 2012-10-31