--- layout: fc_discuss_archives title: Message 43 from Frama-C-discuss on March 2011 ---
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