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



Le 04/11/2011 09:55, Boris Hollas a ?crit :
> 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.
>

You're right, my mistake.

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

Good!

Then now, using why3ide, and "split" button, is everything proved or not?
If not, could you send more details? source code?

- Claude