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