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

Hello Pascal,

2012/5/5 Pascal Cuoq <pascal.cuoq at gmail.com>:
> Unlike the previous statement which, despite being generally false,
> is true about some particular examples, this statement is simply
> always false. The -slevel option has no effects at all on the analysis
> of a linear code without ACSL disjunctions. If you identify a piece of
> linear code on which the option -slevel has an effect, feel free
> to report it as a bug.

OK. I think this time I understood the difference between the two
cases. Beyond use of t[]s, one needs to take account the control
structure and thus the number of paths induced by this control
structure (if (v)... in Boris code, loops in my original code).

> I do not think that the Q&A format is going to work to transmit the
> fundamentals. My case rests on recent discussions on this list
> (including this thread).

:-(

> I would recommend that anyone interested in the subject reads up
> on abstract interpretation, the technique on which the value analysis
> is loosely based (as I think the manual mentions).

I read a bunch of paper on Abstract interpretation, including some of
Cousot & Cousot. But sorry, even if I understand the rough approach, I
cannot understand the fine details, due to lack of time and maybe lack
of some intellectual capabilities.

I think your last remark explains precisely why Value analysis is so
difficult to use: there is no mental model of it (and I'm not even
speaking of a simple one). With Hoare logic approach (WP and Jessie
plugins), you can understand roughly how it works (cf. WP
documentation). Even if the tool itself is much more complicated that
this simple model, it hides all the details and the user can make a
reasoning on tool output (with the help of a few tips).

With Value analysis, one seems to understand how it works but as soon
as one gets to a more complicated/real life example, Value analysis
behaviour is surprising. And the only answer of its developers is "you
need to understand its internals". Right now, its seems that value
analysis is a complex tool that can be only used by its developers at
CEA (with outstanding results, cf. your submission to the robot
debugging contest).

Maybe that's the main difference between expensive tools Polyspace and
Astr?e vs. Value analysis (beyond "correctness", cf. your blog post).
The former targets "real programmers", i.e. people not having a PhD on
Abstract interpretation, while the latter targets other developers
doing static analysis tools. I'm fine with that, but then don't blame
potential users for not understanding your tool and its target.

Please notice that I am not blaming you or other CEA people for this
result. I am only getting what I have paid for, i.e. several working
hours. At least I could made my conclusion without the need to
convince my hierarchy, get a budget to buy the tool, try to justify
it, etc.

And no need to respond to this email, its no worth your time neither mine.

Best regards,
david