--- layout: fc_discuss_archives title: Message 57 from Frama-C-discuss on March 2009 ---
Hello all, Beware! if you run this example is this in the current Lithium version, you have to be careful with the warning issued : Warning: [Jessie plugin] variant for recursive function ignored Indeed, "decreases" clauses are currently unsupported by the Jessie plugin. A more complete answer follows. - Claude Jens Gerlach wrote: > Hello Boris, > > the language specification of ACSL > (http://frama-c.cea.fr/download/acsl_1.4.pdf) contains on page 38 > the faculty function with the follwing specification. > > /*@ requires n <= 12; > @ decreases n; > @*/ > int fact(int n) > { > if (n <= 1) return 1; > return n * fact(n-1); > } > > When I run jessie on this example, then it can verify > that the call of "fact" inside the function body satisfies the > "precondition for user call". > This is of course much less then you asked for. > > Let's keep trying... > > Regards Jens > > > Am 18.03.2009 um 11:56 schrieb Hollas Boris (CR/AEY1): > >> Hello, >> >> I use Spec# with Boogie and the Z3 SMT-solver as back-end. Yet, I >> haven't found a way to verify recursive functions. Therefore, I wonder >> whether this is possible with frama-c and the Jessie plugin. >> >> For example, consider the following recursive implementation of the >> factorial function: >> >> static int fac(int n) >> requires n >= 0; >> ensures result == product {int i in (1..n); i}; >> { >> if(n==0) return 1; >> else return n*fak(n-1); >> } >> >> Spec# is not able to prove the postcondition using default settings. >> Furthermore, I don't know if I can instruct Spec# or the provers to >> induce on n. >> >> Would frama-c be able to verify the function above? >> >> Cheers, >> Boris >> >> _______________________________________________ >> Frama-c-discuss mailing list >> Frama-c-discuss at lists.gforge.inria.fr >> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss > > > > ------------------------------------------------------------------------ > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss -- Claude March? | tel: +33 1 72 92 59 69 INRIA Saclay - ?le-de-France | mobile: +33 6 33 14 57 93 Parc Orsay Universit? | fax: +33 1 74 85 42 29 4, rue Jacques Monod - B?timent N | http://www.lri.fr/~marche/ F-91893 ORSAY Cedex |