--- layout: fc_discuss_archives title: Message 5 from Frama-C-discuss on January 2010 ---
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