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

  • Subject: [Frama-c-discuss] frama-c -wp got stuck
  • From: nicolas.marti.japon at gmail.com (Nicolas Marti)
  • Date: Wed, 30 Jan 2013 08:17:17 +0900
Dear all,

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;

 */

Regards,

   Nicolas
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130130/a2325568/attachment.html>