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

  • Subject: [Frama-c-discuss] Jessie plugin - more than 6, 000 VCs generated
  • From: kanig at adacore.com (Johannes Kanig)
  • Date: Mon, 04 Nov 2013 09:41:02 +0100
  • In-reply-to: <525F8DA9.4080702@inria.fr>
  • References: <CAP6nMJSdSknD8vZDppXi0aNz55zmyi_98ajThBmcMOn3Buks7Q@mail.gmail.com> <525F8DA9.4080702@inria.fr>
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>