--- layout: fc_discuss_archives title: Message 31 from Frama-C-discuss on October 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Is there any method not to initalize all global variables while doing value analysis?



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