--- layout: fc_discuss_archives title: Message 17 from Frama-C-discuss on May 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Issue understanding Value analysis approximation on loop bounds



Hi Pascal,

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.

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. BTW, the Frama-C manual already 
explains -slevel so that a user can understand where it applies or not.

> 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

Not to say that you know exactly what is going on at precision level 0, 
1, 2 or 3, but it gives some clues.

-- 
Yannick Moy, Senior Software Engineer, AdaCore