--- layout: fc_discuss_archives title: Message 88 from Frama-C-discuss on June 2009 ---
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