--- layout: fc_discuss_archives title: Message 30 from Frama-C-discuss on March 2015 ---
On Mon, Mar 30, 2015 at 04:55:00PM +0200, Claude Marche wrote: > > > Le 30/03/2015 14:12, Fritjof Bornebusch a ?crit : > >Hi, > > > >is there a way to verify recursive functions regarding overflows. > > There is nothing special about recursive functions that would make proving > absence of overflows more difficult than for non-recursive ones. > > >If I remove the #pragma statement in this example: > >https://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:frequently_asked_questions#how_do_i_verify_a_recursive_function > > > >the verification fails. > > Of course, since this code overflows as soon as the argument is larger than > 12. (assuming "int" is 32-bit). > > Here is a possible way to handle this. To prove the lemma, you need Z3. > Thank you for that. Is there a way why Z3 is needed? > > /*@ axiomatic Factorial { > @ logic integer factorial(integer n); > @ axiom factorial_0: factorial(0) == 1; > @ axiom factorial_succ: > @ \forall integer n; n > 0 ==> factorial(n) == n * factorial(n-1); > @ } > @*/ > > /*@ lemma fact_bound: \forall integer n; 0 <= n <= 11 ==> > @ 1 <= factorial(n) <= 39916800; > @*/ > > /*@ requires 0 <= n <= 12; > @ decreases n; > @ ensures \result == factorial(n); > @*/ > int fact(int n) { > if (n == 0) return 1; > return n * fact(n-1); > } > > > -- > Claude March? | tel: +33 1 69 15 66 08 > INRIA Saclay - ?le-de-France | > Universit? Paris-sud, Bat. 650 | http://www.lri.fr/~marche/ > F-91405 ORSAY Cedex | > _______________________________________________ > 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 -------------- next part -------------- A non-text attachment was scrubbed... Name: not available Type: application/pgp-signature Size: 819 bytes Desc: not available URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150330/ae3a3451/attachment-0001.sig>