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

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?

If I prefix each "//" line by Frama-C "//@", Frama-C does not accept
them (syntax error).

====
/*@ requires \valid(w+(0..79));
 */
int main(unsigned int w[])
{
  //@ ghost unsigned int data[80];
  //@ ghost int i;

  /*@ ghost
      //@ loop invariant 0 <= i < 80 && \forall integer j; 0 <= j < i
==> w[j] == data[j]; loop assigns i, data[0..79];

      // // I would prefer this form:
      // loop invariant 0 <= i < 80;
      // loop invariant
      //     \forall integer j; 0 <= j < i ==> w[j] == data[j];
      // loop assigns i, data[0..79];
      for (i = 0; i < 16; i++) { data[i] = w[i]; };
  */

  //@ assert w[0] == data[0];

  return 0;
}
====

Best regards,
david