--- layout: fc_discuss_archives title: Message 31 from Frama-C-discuss on October 2012 ---
Thank you for your kindly help. I can't remember whether I installed Zarith or not when I install frama-c. To be in the safe side , I reinstalled frama-c by configuring zarith. In reality, I developed a plugin to calculate some kinds of metrics at function-level. My plugin is depend on value analysis result and need to set each function as entry(main) function for calculate those metrics.So I use option "-lib-entry -main f" for each function. The speed is the biggest problem I encountered. Maybe this system (vim-6.2) which I analysis is too complicate for frama-c. I have use the following options to speed up value analysis: 1. -slevel 10000 2. -memexec-all 3. -memory-footprint 3 Even though, still a little too slow. Some functions need more than half an hour to do the value analysis. I think the best subject the linux-kernel. I really really want to computes those metrics of functions in Linux-kernel. Unfortunately, frama-c can 't support the extension "Length of array size is zero" in linux-kernel source code. So I give up to using linux-kernel as an experimental subject. Is there any method to ignore those errors like "length of array size is zero" and continue to do value analysis? Thank again for advance! ------ Ben 2012-10-31 > > 1. Compile vim-6.2 with option "./configure && make CC="gcc > -save-temps". > > This is a good way, as long as Frama-C can parse the standard headers > (stdlib.h, ...) on your system. > > > 2. For each function f in each temp file filename.i in vim-6.2, treat > > it as the main function and do the value analysis by use the following > > command to do value anlaysis: > > > > "frama-c -lib-entry -main f -val filename.i" > > This will make sense for functions that do not expect complicated chained > data-structures (either as argument or in globals). > > > for analyzing each function f in file, frama-c will initialize all > > global variables in that file. > > That is true. The value analysis is not optimized for analyzing small parts of a > program with lots of globals (which filename.i is, because of all the included > headers). > > The initial state computation could be factored out for each filename.i. > I do not know any way to do this with the command-line in Oxygen, but if there > was a way, it would look like this: > > frama-c -lib-entry filename.i -val-compute-initial-state -save > filename_initial.state > > Then, for each function f: > > frama-c -load filename_initial.state -main f -val > > It should already be possible to do the equivalent of this programmatically (by > writing a custom plug-in) but I do not recommend this solution. > > Apart from this unimplemented idea, using Antoine Min?'s Zarith library makes > the value analysis faster. This include the generation of the initial state. > Are you using it? I enable the Zarith library by configuring Frama-C Oxygen with > the command ./configure > --enable-zarith=/usr/local/Frama-C/ocaml-4.00.1p/lib/ocaml/zarith > where /usr/local/Frama-C/ocaml-4.00.1p/lib/ocaml/zarith is the directory > where I installed Zarith. > > Get the current SVN snapshot of Zarith from here: > http://forge.ocamlcore.org/scm/?group_id=243 > > Pascal