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] Help on handling unknown proof

  • Subject: [Frama-c-discuss] Help on handling unknown proof
  • From: tienhm at gmail.com (Tien Hoang Minh)
  • Date: Wed, 24 Jun 2009 11:09:17 -0400
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