Minor AutoValue unsoundness

[superaxander]

I just figured out a way in which AutoValue is a bit unsound if we have an abstract method like this:

class A {
    int a;
    int b;
}

context p != null;
context AutoValue(p.a);
ensures p.b == 2;
void foo(A p);

Then the AutoValue will act as if its \polarity_dependent(false, true) while verifying the welldefinedness of the method because there are no heap chunks present in that context. When this method is called the welldefinedness is reverified in the context of the call-site which must contain a relevant heap chunk because of the AutoValue in the precondition. Therefore the unsoundness is that we if we have an abstract method that is never called its well-definedness will not be checked. For now this is probably not a big problem but if viperproject/silicon#700 is merged and we end up using that flag then this might become a problem.

This luckily also not a problem if the method is not abstract since then there will be context with a heap chunk inside the method body which will make it so that inhaling the forperm expressions is sound again.

[superaxander]

I ended up finding another source of unsoundness which I fixed in #1252 by not allowing AutoValue to be used with other permission annotations for the same permission. It'd be great to find another way of encoding it so that this problem doesn't occur and so that it can be mixed with other permission annotations.