--- layout: fc_discuss_archives title: Message 4 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?



Le lun. 04 janv. 2010 11:02:38 CET,
"David A. Wheeler" <dwheeler at dwheeler.com> a ?crit :

> But two adjacent "//@" lines do NOT work.  What's more,
> this gave an incredibly misleading error message in a far later
> line, and that's why I thought loop variants were unsupported.

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.

-- 
Virgile Prevosto
Ing?nieur-Chercheur, CEA, LIST
Laboratoire de S?ret? des Logiciels
+33/0 1 69 08 82 98