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] Code doesn't verify anymore with new Frama-C/Jessie release

On Thu, 2011-11-03 at 13:11 +0100, Claude Marche wrote:
> From your message, I guess you mean that you are using the Why3
> backend (since Vampire is not available in Why 2.30)
yes, I had that problem with why3. However, Vampire also works with the
why2-gui.

> First of all, you may want to check that your proofs still work with
> the former Why 2.30 back-end, using frama-c -jessie -jessie-atp=gui
indeed, with the why2 back-end, the code verifies as before.

-- 
Best regards,
Boris