Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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);
}