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: dmentre at linux-france.org (David MENTRE)
  • Date: Tue, 8 May 2012 18:53:25 +0200
  • In-reply-to: <CAOH62Jg1zWJscGe=qZ4WMM=DrOWrcEE_jmbs5B4Gha73QfPUWg@mail.gmail.com>
  • References: <CAOH62JhAyq8W1m8T-U6Sb7hddQS2hW6LqrM2jP7JUf29yhbfxQ@mail.gmail.com> <CAC3Lx=bDY5LLYqLL5Nbiper_yjC81mcpFPkxarQQxiG+Qf3r4w@mail.gmail.com> <CAOH62Jh=knRUk5M3Tcf9R+9Q=nfhnS4zsFoXMzyuu0hJtBgPcQ@mail.gmail.com> <4FA78C2E.90301@adacore.com> <CAOH62Jg1zWJscGe=qZ4WMM=DrOWrcEE_jmbs5B4Gha73QfPUWg@mail.gmail.com>
Hello Pascal,

2012/5/7 Pascal Cuoq <pascal.cuoq at gmail.com>:
> 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.

Glad to know. As an engineer, I am perfectly fine with this approach.
I'll used it then.


> 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.

Unfortunately for me my claim was unsubstantiated. I have never used
PolySpace neither Astr?e, just recalled an old presentation on
PolySpace 10 or 15 years ago, where the user interface was very simple
at that time (4 analysis levels, 4 colours for the result).

Best regards,
david