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] Plugins in next Frama-C?
- Subject: [Frama-c-discuss] Plugins in next Frama-C?
- From: pascal.cuoq at gmail.com (Pascal Cuoq)
- Date: Thu, 7 Oct 2010 07:44:29 -0700
- In-reply-to: <1286450446.7104.251.camel@iti27>
- References: <AANLkTikw8pjgcE3LS1tqDebwktuECBkoFfLLRAw=UEFu@mail.gmail.com> <AANLkTimrtkSEWFs5br=YJn8QXa5Y8pbr8KbKwQv6tDkA@mail.gmail.com> <1286450446.7104.251.camel@iti27>
On Thu, Oct 7, 2010 at 4:20 AM, Boris Hollas <hollas at informatik.htw-dresden.de> wrote: > On Wed, 2010-10-06 at 12:37 -0700, Pascal Cuoq wrote: >> There will be a new weakest precondition plug-in alongside Jessie, >> with different strengths and weaknesses. It will of course make use of >> the same ACSL contracts. > > How does this wp-plugin differ from Jessie? There is not much more that can be said without raising even more questions. For the simple functions, it will be possible to write annotations that can be verified by both Jessie and this unnamed plug-in. The difference will only be in the difficult cases. The differences will be clear when this plug-in is announced, and you will only need to look at the code to see which plug-in is likely to provide the best results, so that you do not have to choose at random. Pascal
- Prev by Date: [Frama-c-discuss] Alt-ergo 0.92.1, Frama-C/Why package on Fedora
- Next by Date: [Frama-c-discuss] Alt-ergo 0.92.1, Frama-C/Why package on Fedora
- Previous by thread: [Frama-c-discuss] Plugins in next Frama-C?
- Next by thread: [Frama-c-discuss] Alt-ergo 0.92.1, Frama-C/Why package on Fedora