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?

  • Subject: [Frama-c-discuss] Syntax of annotations in ghost code?
  • From: virgile.prevosto at m4x.org (Virgile Prevosto)
  • Date: Wed, 11 Sep 2013 10:13:57 +0200
  • In-reply-to: <CAC3Lx=aDAioqVN-v9+LAd5o0CVqTrbEouWW7pLfEyyZh9xsCxQ@mail.gmail.com>
  • References: <CAC3Lx=aDAioqVN-v9+LAd5o0CVqTrbEouWW7pLfEyyZh9xsCxQ@mail.gmail.com>
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