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

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