Many missing semicolons

[tlringer]

Hi all, continuing with the tutorial now. I've run every single cn file I've encountered throughout. I've noticed there have been a lot of missing semicolons, and so sometimes I get confusing errors until I fix that. For example, consider transpose.broken.c in the "Resource Interference" section:

struct point { int x; int y; };

void transpose (struct point *p)
/*@ requires take s = Owned<struct point>(p)
    ensures take s2 = Owned<struct point>(p);
            s2.x == s.y;
            s2.y == s.x
@*/
{
  int temp_x = p->x;
  int temp_y = p->y;
  /*@ assert(false); @*/
  p->x = temp_y;
  p->y = temp_x;
}

If I try to run this, I get this error:

(base) talia@xenon-v4:~/cn-tutorial/build/exercises$ cn transpose.broken.c 
transpose.broken.c:5:5: error: unexpected token after ')' and before 'ensures'
parsing "condition": seen "CN_TAKE LNAME VARIABLE EQ resource", expecting "SEMICOLON"
    ensures take s2 = Owned<struct point>(p);
    ^~~~~~~ 

After fixing the first missing semicolon, if I try to run this again, I get this error:

(base) talia@xenon-v4:~/cn-tutorial/build/exercises$ cn transpose.broken.c 
transpose.broken.c:8:1: error: unexpected token after 'x' and before ''
Please add error message for state 1056 to parsers/c/c_parser_error.messages
@*/
^

After fixing the second missing semicolon, finally I get the error I am expecting where the false assertion cannot be satisfied.

I believe I encountered this at least five times so far, so I would recommend going through the tutorial and checking for missing semicolons.

[septract]

A few weeks ago made a syntax change with CN to require ; at the end of requires / ensures blocks. But it seems the change was only propagated to the working examples, not the examples that are (deliberately) broken. So I expect any file with a name *.broken.c will be incorrect.

The solution here is:

• The examples should be updated to follow the new syntax.
• The CI script here should check all examples return the expected value, not just working examples. At the moment examples marked broken are skipped.