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