--- layout: fc_discuss_archives title: Message 67 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 David,

2013/9/11 David MENTRE <dmentre at linux-france.org>:
> I played a little with ghost code. However, the usable syntax for
> formal annotations in ghost code is not clear to me.
>
> In the following example, everything is proved with -wp -wp-rte. Is it
> possible to put the ghost code formal loop contract line ("//@ loop
> invariant 0 <= i < 80 && \forall integer j;...") into a multi-line
> format for better readability?
>

No, it's not possible: Each //@ is supposed to be a self-contained
annotation. Moreover, as you can only have one loop annotation tied to
a given loop,
//@ loop invariant foo;
//@ loop invariant bar;
//@ loop assigns x;
for (...)
is not possible either: there are three distinct annotations for the same loop.

I don't think that tying together two consecutive //@ lines is
desirable, since we would end up with other issues, such as
//@ assert foo;
//@ loop invariant bar;
for (...)

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.

Allowing /@ @/ as mentioned on the ACSL document might prove to be a
bit technical but should be doable.

Best regards,
-- 
E tutto per oggi, a la prossima volta
Virgile