--- layout: fc_discuss_archives title: Message 36 from Frama-C-discuss on August 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Jessie proof obligation not discharged?



Dear Claude,

At Thu, 23 Aug 2012 10:17:19 +0200,
Claude Marche wrote:
>
>
> Generally speaking, to "debug" such a proof, I launch an interactive
> prover like Coq. By trying to do that proof by hand you wuold have seen
> the mistake.

thanks for sharing this type of advice, greatly appreciated!

> And launching on a PO is greatly greatly easier with Why3 instead of
> Why2 : so I'd like to suggest to try using Why3 back-end of jessie !
> (which is indeed the only one which is maintained and evolves)

OK, I switched.

Best regards,

Marko
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 198 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20120823/20605b1d/attachment.pgp>