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