Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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