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
- References:
- [Frama-c-discuss] Issue understanding Value analysis approximation on loop bounds
- From: pascal.cuoq at gmail.com (Pascal Cuoq)
- [Frama-c-discuss] Issue understanding Value analysis approximation on loop bounds
- From: dmentre at linux-france.org (David MENTRE)
- [Frama-c-discuss] Issue understanding Value analysis approximation on loop bounds
- From: pascal.cuoq at gmail.com (Pascal Cuoq)
- [Frama-c-discuss] Issue understanding Value analysis approximation on loop bounds
- From: moy at adacore.com (Yannick Moy)
- [Frama-c-discuss] Issue understanding Value analysis approximation on loop bounds
- From: pascal.cuoq at gmail.com (Pascal Cuoq)
- [Frama-c-discuss] Issue understanding Value analysis approximation on loop bounds
- Prev by Date: [Frama-c-discuss] Issue understanding Value analysis approximation on loop bounds
- Next by Date: [Frama-c-discuss] Issue understanding Value analysis approximation on loop bounds
- Previous by thread: [Frama-c-discuss] Issue understanding Value analysis approximation on loop bounds
- Next by thread: [Frama-c-discuss] Issue understanding Value analysis approximation on loop bounds
- Index(es):