[CN] Block should allow omitting C-type like owned
Closed this issue · 1 comments
dc-mak commented
Owned can omit C types in this context and Block is just an unintialised Owned, so it should allow it too.
13:16 ➜ cerberus git:(master) cat block_no_annot.c && cn verify block_no_annot.c
void f(int *p)
/*@ requires take V = Block(p);
ensures take V2 = Block(p);
@*/
{ }
block_no_annot.c:2:28: error: unexpected token after 'Block' and before '('
parsing "pred": seen "CN_BLOCK", expecting "LT ctype GT"
/*@ requires take V = Block(p);
^