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

[peterohanley]

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]

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

[cp526]

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.

[peterohanley]

The accesses part of this is now impeding TA2 work, I would appreciate a fix even for just this part.

[septract]

Bumping this issue as it's now also blocking work on the TA2 Mission Key Management example.

Here's a distilled example of the problem (derived from policy_add in mission_key_management/policy.c, here). Suppose we have three files: libfile.c, libfile.h, clientfile.c.

libfile.c:

#include "libfile.h"

int foo(int i) 
/*@
accesses myval; 
requires myval == 1i32; 
         i == 1i32; 
ensures  return == 0i32; 
@*/
{
  if (i == myval) return 0; 
  else return 1; 
}

clientfile.c:

#include "libfile.h" 

int bar() 
/*@ 
accesses myval; 
@*/
{ 
  myval = 0; 
  int i = foo(0); 
}

libfile.h

int myval = 0; 

int foo(int i); 
// Should be able to write spec here 

We can't verify clientfile.c because foo() doesn't have a specification in scope. But if we try to add a specification to libfile.h, we can't because it would require an accesses annotation.

@cp526 @dc-mak and others in the CN team - this is a blocker on TA2 work for both @peterohanley and myself. Could you look at this and make an assessment about how difficult it would be to fix?

[dc-mak]

On it. Apologies for the inconvenience. It's not just a grammar change - code needs to be moved from the frontend to the backend. Nothing conceptually difficult, best guess is that it will probably take a few (2-3) days.

[septract]

Thanks @dc-mak - once you have this in prototype, I have an example in the OpenSUT we can use to test it.

[septract]

@dc-mak also note there was some talk of removing the accesses notation altogether.

[dc-mak]

Can you check out #892 and test it locally? The code's ready to go but I still need to add a few tests for the new behaviour.