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] frama-c -wp got stuck

Hello,

On 01/30/2013 12:17 AM, Nicolas Marti wrote:
> I just happened to build an example where frama-c (more precisely using
> the wp plugin) got stuck (I stopped after ~10mins and ~2Go).
> I kind of understand that the Typed model is experimental, which might
> explains the behavior.
> I am using the frama-c-Oxygen.
> Bellow lies the content of the file that I process with the following
> options: -wp -wp-model Typed -wp-proof none
>
> /*@
>
> logic integer pow(integer x, integer y) = y == 0 ? 1 : (x * pow(x, y - 1));
>
> lemma pow_0: \forall integer x; pow(x, 0) == 1;
>
> */

Thanks for your bug report. I reproduced your issue with Oxygen. This 
bug seems to be already fixed in our SVN. The fix will be part of the 
next Frama-C public release (hopefully soon).

Please, do not hesitate to use http://bts.frama-c.com instead of this 
list in order to report bugs (see also 
http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines).

Best regards,
Julien