--- layout: fc_discuss_archives title: Message 29 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?



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>