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: pascal.cuoq at gmail.com (Pascal Cuoq)
  • Date: Tue, 30 Oct 2012 08:14:53 +0100
> 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