Resources are not allowed in \unfolding

[bobismijnnaam]

The following code:

resource x() = true;
requires x() ** x();
requires \unfolding x() \in x();
void m();

Gives the following error on the ast branch:

[ERROR] Viper has crashed: java.lang.RuntimeException: Unexpected expression acc(x(), write) cannot be symbolically evaluated

A similar program in viper also gives the error that you cannot have an impure expression in an unfolding expression. VerCors should probably disallow this and prevent it in the typechecking phase. Alternatively we can ask the viper team if this is a bug or if it can be extended to allow resources inside unfolding.

[pieter-bos]

Seems to me there are reasonable cases where you would want this:

class C2 {
  resource p() = Perm(x, write) ** Perm(y, write);
  int x;
  int y;
}

class C1 {
  resource p() = Perm(x, write) ** Perm(y, write) ** Perm(z, write);
  int x;
  int y;
  C2 z;

  //@ requires p() ** \unfolding p() \in z.p();
  void test();
}

Although in this case sensible alternatives might be making the predicates inline, or making C1 own C2 by including z.p() in C1.p. If you were thinking of different scenarios please include them.

[pieter-bos]

Related: viperproject/silver#606