--- layout: fc_discuss_archives title: Message 69 from Frama-C-discuss on September 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Syntax of annotations in ghost code?



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