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

Hi,

 From your message, I guess you mean that you are using the Why3 backend 
(since Vampire is not available in Why 2.30)

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

Second, when using Why3 backend, that's true that VCs are slightly 
different, but the most important thing
is that they are not automatically split into pieces when they are 
conjunctions. So, when a VC is not proved, the first thing to try is the 
"split" button of why3 ide.
See both jessie manual ("tutorial" part, 
http://krakatoa.lri.fr/jessie.html#htoc5) and Why3 manual 
(https://gforge.inria.fr/docman/view.php/2990/7635/manual.pdf,
Section 1.2)

If you did all that already, then further investigation is needed. I'll 
be happy to help but I need more details: input source if possible, and 
which VC you can't prove.

Regards,

- Claude



Le 03/11/2011 09:42, Boris Hollas a ?crit :
> Hello,
>
> I have code that verified with the previous release of Frama-C/Jessie 
> + Alt-Ergo + Simplify, but not with the current release, even with a 
> prover timeout of 5 minutes. I use Alt-Ergo, Simplify and Vampire as 
> back-end provers. Before I try adding more specification, are there 
> other options I have? Has the new why release, which I installed 
> together with why3, changed the way in which VC are generated?
> -- 
> Best regards,
> Boris
>
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss

-------------- section suivante --------------
Une pi?ce jointe HTML a ?t? nettoy?e...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20111103/e4253fea/attachment.htm>