search

gradual-verification / gvc0

Gradually Verified C0
6 stars 5 forks source link

Recursive predicates should fail due to separation rather than infinite recursion if separation failure applies #49

Open jennalwise opened 1 year ago

jennalwise commented 1 year ago

When erroring at run-time for this incorrectly specified predicate:

predicate acyclicSeg(Node *s, Node* e) =
  (s == e) ? true : acc(y->val) && acc(y->next) && acyclicSeg(s,e);

The GVC0 produces a C0 error for an infinite recursion, which is correct for how our tool is currently implemented. However, if we checked separation first or in tandem with checking ownership in this predicate (we don't do this currently, checking separation happens after checking ownership), then we could catch this error without infinite recursion and give a better error message.

jennalwise commented 1 year ago

The best solution for this is to have the backend give separation information alongside other run-time check information.