--- layout: fc_discuss_archives title: Message 30 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



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>