--- layout: fc_discuss_archives title: Message 23 from Frama-C-discuss on October 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Plugins in next Frama-C?



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