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] Issue understanding Value analysis approximation on loop bounds

On 05/05/2012 06:53 PM, Pascal Cuoq wrote:
>>
>> the option works as described: for a given program, increasing
>> the value of -slevel makes the analysis more precise (you said
>> something about 10000). You do not need to understand what
>> it does to use it. You need to know that a higher level usually
>> means more resources consumed and better precision.

On Mon, May 7, 2012 at 10:47 AM, Yannick Moy <moy at adacore.com> wrote:
>
> I disagree. Users of static analyzers need to interact with the tool in a
> clever way, not blindly pushing buttons here and there to make the analysis
> "pass" by some miracle.

For this particular option, I beg to differ. It is not as if there was
a second-fucking-best option that the user could try if this one
does not work. OPTION "-slevel" IS THE ONE THAT WORKS.
You don't need to know what it does (although, reading again my tutorial,
I realize it does summarize what the option does) because you
DO NOT choose it among a selection of alternatives. If you have tried
"-slevel 100" and it wasn't as precise as you expected, you don't
try another option; you try "-slevel 1000".

You don't need to match it carefully to the code being analyzed.
You just use it. It almost always improves precision.
Every alternative to improve precision is painful.
IT'S THE ONE THAT WORKS.

Do I know what the code in gd_full_bad.c in
http://blog.frama-c.com/index.php?post/2012/03/12/Minimizing-alarms
does? No.I didn't match the analysis options carefully to the code being
analyzed. I didn't even read the stupid thing. But I analyzed it
precisely enough that there was only one alarm, a true
alarm, the bug to find in this particular *_bad.c example from
a benchmark.

How did I do it? I used option -slevel. Forget about all the other options,
from that blog post and from any other source of documentation.
Get a fast computer. Stub missing functions properly. Use -slevel.
If there are still false alarms when it becomes unbearably slow,
suck it up and review them. End of methodology.

>> I would be delighted to know what single global option you used
>> to make PolySpace or Astr?e analyse your example(s), if only
>> to mention their respective names casually at parties.
>
>
> Looking at the reduced example of David, I think PolySpace could prove the
> absence of run-time errors, because it has a domain of linear relations
> between variables. For PolySpace precision options, their manual is doing a
> good job I think:
>
> http://www.mathworks.fr/help/toolbox/polyspace/ada_ref/brid6de.html

This is an interesting link, but this was not my question.
My question was about what PolySpace/Astr?e options David had used
to actually analyze his examples that made him think these tools
were more engineer-friendly. I am certain that they can each do it.
I am just saying that for the value analysis, the deal is simple?insultingly
simple for an engineer, probably: Stub. Use -slevel. If there are alarms,
review them. Using this methodology, the value analysis' score in
Nitrogen on his reduced example is 0.72s, using a large enough
slevel (I forget the value), on a 2006 computer. I would like to
know how much trouble it is to actually get the result with a particular
analyzer, not whether it can theoretically provide it.

But perhaps this example is not interesting, because it was
reduced too much. Let us consider the original then.
But already, reading from the PolySpace documentation you
linked, more options may become necessary. Perhaps the
contents of the arrays manipulated in the nested loops are
interesting. It may be necessary to use the
"Max size of global array variables" option then, perhaps
fiddle with other parameters. With Frama-C's value analysis,
it's simple: either it succeeds with -slevel, or it will be a lot of work
and require expertise to improve precision, so don't try it:
save your time for reviewing the alarms.

>From what I hear, Frama-C's value analysis succeeded
with just -slevel on David's original example, just a bit slowly
or something.
So I would be really really interested in the ACTUAL results
he got with PolySpace and Astr?e that make him think they are
more engineer-friendly.


I have long been interested in static analyzers comparisons,
to the point of co-signing a short pamphlet recently:
http://blog.frama-c.com/index.php?post/2012/04/29/Benchmarking
One pitfall so obvious that we do not even mention would be
comparing actual runs of one analyzer with what others are
supposed to do "on paper". It doesn't matter whether the comparison is
about results or usability: most techniques look promising on paper.
Surely he was not expressing thoughts on how the three compare
after having actually tried only one of them?

Pascal