#include <civlc.cvh>
#include <memory.cvh>

void inc(int* n);

void dec(int* n);

/*@ depends_on \anyact;
  @ assigns \object_of(a), \object_of(b);
  @*/
void test(int* a, int* b);

/*@ depends_on (\write(n)+\read(n))-(\call(inc, n)+\call(dec, n));
  @*/
void foo(int* n);