--- layout: fc_discuss_archives title: Message 26 from Frama-C-discuss on March 2015 ---
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. /*@ 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 |