--- layout: fc_discuss_archives title: Message 88 from Frama-C-discuss on June 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Help on handling unknown proof



Hi all,
I used Frama-C/Jessie/Alt-Ergo in my C project, when verifying there
are a lot of unknown and time out proof, is there any suggestion for
me where to begin to solve all of these, is there any document about
this issue. I attach to this email a small example. Please help me to
clear all the unknown proof.
In another C code of my project, I do not use any exception, but when
verifying, I have the following warnings
Calling VCs generator.
why -alt-ergo [...] why/test.why
File "why/test.why", line 1917, characters 5-16:
warning: no postcondition for exception Goto__L_exc; false inserted
File "why/test.why", line 2530, characters 4-8:
warning: no postcondition for exception Goto__L_exc; false inserted
are these warnings really important, how can I avoid them.
Thank you very much.
-------------- next part --------------
A non-text attachment was scrubbed...
Name: a.c
Type: text/x-csrc
Size: 216 bytes
Desc: not available
Url : http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090624/c935d333/attachment.c