--- layout: fc_discuss_archives title: Message 14 from Frama-C-discuss on January 2013 ---
[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