int foo(int x)
/*@
requires
x + n - n < MAXi32();
cn_ghost i32 n; true;
ensures
return == x + 1i32;
@*/
{
return x + 1;
}
return code: 1
tests/cn/ghost_bad_ordering.error.c:5:5: warning: experimental keyword 'cn_ghost' (use of experimental features is discouraged)
cn_ghost i32 n; true;
^~~~~~~~
tests/cn/ghost_bad_ordering.error.c:5:5: error: unexpected token after ';' and before 'cn_ghost'
Please add error message for state 1696 to parsers/c/c_parser_error.messages
cn_ghost i32 n; true;
^~~~~~~~