--- layout: fc_discuss_archives title: Message 69 from Frama-C-discuss on September 2013 ---
Hello Virgile, 2013/9/11 Virgile Prevosto <virgile.prevosto at m4x.org>: > No, it's not possible: Each //@ is supposed to be a self-contained > annotation. OK, thanks. > A possibility, for both ghost and non-ghost code, would be to use '\' > at the end of a one-line annotation to indicate that it is to be > continued on the next line, e.g. > //@ loop invariant foo; \ > //@ loop invariant bar; \ > //@ loop assigns x; > It should be possible to add it without too much changes in the lexer > and parser. That's an interesting option. > Allowing /@ @/ as mentioned on the ACSL document might prove to be a > bit technical but should be doable. Ah, that's explain why I wasn't able to use it. ;-) Best regards, david