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: Fri, 26 Oct 2012 10:20:38 +0800
Hi, everybody:

 

I use Frama-c to analysis vim-6.2 project.

The problem which I met is the speed of value analysis.

The procedure for analyzing vim is:

1.     Compile vim-6.2 with option "./configure && make CC="gcc
-save-temps".

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"

 

As we know, value analysis is context sensitive. At the same time, for
analyzing each function f in file, frama-c  will initialize all global
variables in that file.

So this will requires a lot of time to do the analysis.

 

In most cases, not all global variables are used in the function f. So I'd
like to know is there any method to improve the speed of value analysis by
not initializing those global variables which the main function f is not
used?

 

Thanks for advance.

 

------

Ben

2012-10-26

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20121026/b303d46c/attachment.html>