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

}