Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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?

  • Subject: [Frama-c-discuss] Is there any method not to initalize all global variables while doing value analysis?
  • From: abiao.yang at gmail.com (Ben)
  • Date: Wed, 31 Oct 2012 01:26:12 +0800
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