--- layout: fc_discuss_archives title: Message 5 from Frama-C-discuss on November 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Feature or bug?



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