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

[Frama-c-discuss] small question



Hi,
As g is recursive, you have to prove its termination. You may add a decrease clause to the specification of g. 
Cheers
Benjamin Monate
CEA LIST
Head of Software Safety Laboratory

Le 18 mars 2011 ? 08:55, "Romain Jobredeaux" <Romain.Jobredeaux at supelec.fr> a ?crit :

> Hi all,
> 
> Trying the jessie plugin on this relatively straightforward program and annotations, I get a safety condition "0<0" on g and don't really understand where it comes from...
> 
> Can you help me out ?
> 
> Romain Jobredeaux
> 
> #include <stdio.h>
> #include <stdint.h>
> 
> 
> /*@ requires x >= 0;
>  @ requires x < 10;
>  @ ensures \result == x * ( x + 1 ) / 2; */
> int g ( uint8_t x )
> {
> 
>  if ( x == 0 )
>    return 0;
>  else
>    return x + g ( x - 1 );
> 
> }
> 
> 
> /*@ ensures \result == 36; */
> int main ()
> {
> 
>  int i = g ( 8 );
> 
>  return i;
> 
> }
> 
> 
> 
> 
> _______________________________________________
> 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