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

[Frama-c-discuss] Res: Feature or bug?



Am 09.11.2009 um 17:54 schrieb Claude Marche:

> 
> Could you explain why this behavior really annoys you ?

I wouldn't use the word "annoy", but looking at my original example (see below)
the different answers from the provers might appear at first sight as inconsistent.

It also reminds me of the "green follows orange" feature of Polyspace (http://www.mathworks.se/access/helpdesk/help/toolbox/polyspace/c_ug/brj0wna-1.html)
which in my experience bothers some users.

Regards Jens

/*@
   requires 0 <= x;
   ensures   0 <= \result;
*/
int foo(int x);

void bar()
{
   foo(-1);
   foo(-1);
}