ai_annot.i

/* run.config*
   STDOPT: #"-scope-verbose 2 -eva-remove-redundant-alarms -eva-context-width 3"
   */


int u,v,w;

int main(int x,int *p) {
  /*@ assert x >=0; */
  /*@ assert \valid(p+1); */
  /*@ assert \valid_read(p+2); */
  *(p+1)=x;

  return x+*(p+2);
}