--- layout: fc_discuss_archives title: Message 30 from Frama-C-discuss on October 2012 ---
> 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