--- layout: fc_discuss_archives title: Message 8 from Frama-C-discuss on November 2011 ---
[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