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] 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>