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

  • Subject: [Frama-c-discuss] Issue understanding Value analysis approximation on loop bounds
  • From: moy at adacore.com (Yannick Moy)
  • Date: Mon, 07 May 2012 10:47:42 +0200
  • In-reply-to: <CAOH62Jh=knRUk5M3Tcf9R+9Q=nfhnS4zsFoXMzyuu0hJtBgPcQ@mail.gmail.com>
  • References: <CAOH62JhAyq8W1m8T-U6Sb7hddQS2hW6LqrM2jP7JUf29yhbfxQ@mail.gmail.com> <CAC3Lx=bDY5LLYqLL5Nbiper_yjC81mcpFPkxarQQxiG+Qf3r4w@mail.gmail.com> <CAOH62Jh=knRUk5M3Tcf9R+9Q=nfhnS4zsFoXMzyuu0hJtBgPcQ@mail.gmail.com>
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