--- layout: fc_discuss_archives title: Message 33 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 so much for timely replying me.
In honest, I like frama-c very much. It's so powerful. It is amazing that
value analysis can be so precisely.
I can almost do whatever I want by using this analysis framework.

> You are using Frama-C's value analysis plug-in, a state-of-the-art static
analysis
> component that has been successfully applied to large codebases of
industrial
> embedded C code.

Which industrial embedded C code has been successfully applied?
Is there any large open source codebases have been analysis by using
frama-c?

> But wait! You are not doing a verification of Vim with Frama-C's value
analysis.
> You are using the value analysis in an unconventional fashion to obtain
results
> that you need for something else you want to do.
> Would you say that a hammer is unable
> to handle nails because you tried to smash it on a hundred nails at once
and it
> did not do what you expected?

I'm sorry to use frama-c in a wrong way. Maybe I should first use CIL (C
Intermediate Language) to merge all vim source codes into a single file.
Then, use frama-c to analysis that merged file.
At that situation, I have no need to set that '-main' option for each
function and do value analysis only once.

> > I have use the following options to speed up value analysis:
> > 1.  -slevel 10000
> 
> Do you have any reason to think that this makes the analysis faster?
> I think that the documentation is rather clear on the fact that option
-slevel
> improves precision, usually at the cost of time and memory.
> 

I just try this option for another time. It did not speed up the value
analysis.
I have read the documentation before. 
But when I use the command line: 
'frama-c -value-help'
It shows that:
"...
-slevel <n>  use <n> as number of path to explore in parallel
..."
This makes me misunderstanding and wrongly using this option. 
Thanks for remind me of this option.

> > Is there any method to ignore those errors like "length of array size
> > is zero" and continue to do value analysis?
> 
> The C99 standard says:
> 
> 6.7.5.2 Array declarators
> Constraints
> 
> 1. [...] If the expression is a constant expression, it shall have a value
greater
> than zero.
> 

Thank you. Maybe the linux-kernel version which I analyzed is out of date.

I would like to know if there is anybody have succeed analyzing Linux-kernel
by using your group's tool frama-c before?
I can just successfully saved all temp files of linux-kernel source code by
change the makefile.build file.


Ben
2012-10-31