--- layout: fc_discuss_archives title: Message 67 from Frama-C-discuss on September 2013 ---
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