--- layout: fc_discuss_archives title: Message 13 from Frama-C-discuss on November 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Jessie plugin - more than 6, 000 VCs generated



Hello,

On Thu, 17 Oct 2013 09:11:37 +0200, Guillaume Melquiond <guillaume.melquiond at inria.fr> wrote:
> This gets the number of proof obligations after split from 2189 to 2.
> The fact that there are only two obligations left kind of frightens me,
> so I cannot guarantee that it works correctly.

As the author of the Why3 fastwp, I can look into this if you guys provide me with a Why3 file. 2189 VCs down to 2 sounds strange indeed.

Johannes

-- 
Johannes Kanig <kanig at adacore.com>