--- layout: fc_discuss_archives title: Message 47 from Frama-C-discuss on May 2009 ---
Hello, I tried to prove the following post conditon with Jessie but could not succeed when calling frama-c -jessie-analysis -jessie-gui my_sqr.c on Mac OS X (neither with alt-ergo, yices, and cvc3). Did I miss something obvious? Regards Jens /*@ ensures \result >= 0.0; */ double sqr(double x) { return x * x; } -- -------------- next part -------------- An HTML attachment was scrubbed... URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090519/252aaa19/attachment-0001.htm