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

[Frama-c-discuss] With Why version 2.23, Jessie binary_search example fails. Why?



Virgile Prevosto:
> You're right, the location of the error is completely wrong and we
> have to investigate a bit further. The error message is correct,
> though: you can only have one loop annotation per loop, and the two
> one-line comments are seen as two distinct annotations. The only way to
> have multi-line annotations is to use the /*@ ... */ syntax.

Okay, that makes sense.  Personally, I think //@ without intervening code
should be merged and treated as a single comment.
There's an old bug saying the same thing:
  http://bts.frama-c.com/view.php?id=79
A non-misleading error message would be better than what happens now,
but "doing the right thing" would be even better :-).

I submitted the binary_search documentation bug here:
  http://bts.frama-c.com/view.php?id=365

I believe that binary_search's requirements changed because
termination proofs are now required by default:
  http://bts.frama-c.com/view.php?id=103

--- David A. Wheeler