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 14:49:23 +0800
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