--- layout: fc_discuss_archives title: Message 26 from Frama-C-discuss on March 2015 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] recursive function int overflow




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                    |