--- layout: fc_discuss_archives title: Message 23 from Frama-C-discuss on October 2010 ---
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