Skip to content

[CN] Block should allow omitting C-type like owned #413

@dc-mak

Description

@dc-mak

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);
                           ^

Metadata

Metadata

Assignees

No one assigned

    Labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions