search

rems-project / cerberus

Cerberus C semantics
https://www.cl.cam.ac.uk/~pes20/cerberus/
Other
48 stars 25 forks source link

[CN] specs on declarations have a different syntax from specs on definitions #371

Open peterohanley opened 2 months ago

peterohanley commented 2 months ago

In particular accesses does not work but trusted also does not.

int x;

void f(void)
/*@ accesses x; @*/
{

}

void g(void);
/*@ spec g();
    accesses x;
@*/
% cn accesses_spec.c
accesses_spec.c:10:5: error: unexpected token after ';' and before 'accesses'
parsing "cn_fun_spec": seen "CN_SPEC LNAME VARIABLE LPAREN cn_args RPAREN SEMICOLON", expecting "CN_REQUIRES nonempty_list(condition) CN_ENSURES nonempty_list(condition)"
    accesses x;
    ^~~~~~~~

Looking at the grammar in the documentation, it looks like a declaration spec should refer to function_spec rather than hardcode only requires and ensures.

septract commented 1 month ago

I think the ideal way to resolve this would be to eliminate the distinction between spec and trusted - see #467

cp526 commented 1 month ago

Agreed, we should fix the CN frontend so the syntax for spec includes all the features that specifications on defined functions support.

As commented on #467, trusted and spec have a different purpose, so we should keep both.