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

[jennalwise]

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]

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