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