--- layout: fc_discuss_archives title: Message 71 from Frama-C-discuss on January 2014 ---
Your spec is wrong. Result is always (-1) even when i == 5 (which actually only occurs in lib-entry mode, otherwise i == 0). And there is no RTE to check, as it can be confirmed by value. L. Le 24 janv. 2014 ? 03:36, Dharmalingam Ganesan <dganesan at fc-md.umd.edu> a ?crit : > Hi, > > Thanks for all responses. I'm not sure why the following code cannot considered invalid; I always get "unknown". > > Any comments? > > frama-c -wp -wp-rte non_sense.c -lib-entry > > > > int i = 0; > > /*@ > @ behavior BUG: > @ assumes i == 5; > @ ensures \result == -2; > */ > > int main() > { > if (0 <= i && i <= 10) > { > return -1; > } > > if (i == 5) > { > return -2; > } > > return 0; > } > > _______________________________________________ > 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