--- layout: fc_discuss_archives title: Message 14 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



Dear Johannes,

We have not tried to run the David's suggestion, because we are Frama-C
begginer's users and we do not know how to modify the makefiles. However,
if you could give the hints to do that, we can send you the file.

Best regards
Nanci



On Mon, Nov 4, 2013 at 6:41 AM, Johannes Kanig <kanig at adacore.com> wrote:

> 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.
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131104/39fd84c1/attachment.html>