--- layout: fc_discuss_archives title: Message 5 from Frama-C-discuss on November 2009 ---
Hi, in the following example the function foo is called twice by the function bar and in both cases bar does not fulfill foo's precondition "x >= 0" . ---------------- /*@ requires 0 <= x; ensures 0 <= \result; */ int foo(int x); void bar() { foo(-1); foo(-1); } -------------- However, all provers "proof" that for the second case the precondition is fulfilled (see below). Is this behaviour of Jessie intended? (I am using the Beryllium1 release on Mac OS X.) Regards Jens Gelach -------------- next part -------------- A non-text attachment was scrubbed... Name: results.jpg Type: image/jpg Size: 34561 bytes Desc: not available Url : http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20091105/ae6c55a3/attachment-0001.jpg