gvc0 generates permission-manipulating code based on expressions over mutable data rather than stored variables

[JonathanAldrich]

When making a call to a function with an argument expression like this:

f(x, x->g->h)

if we assume that f has arguments a,b and a precondition myPredicate(a, b), then before the call, gvc0 generates permission code that removes the owned fields in myPredicate(x, x->g->h). This is fine. But if f has that same postcondition, the permission code generated after the call will add back in the owned fields in myPredicate(x, x->g->h).

The problem comes when function f assigns x->g to NULL! Then doing anything with myPredicate(x, x->g->h) will result in a null pointer exception, because the null pointer x->g is dereferenced.

One possible solution is to assign a temporary variable tmp=x->g->h and then do any operations after the call in terms of temp, i.e. add back in the owned fields in myPredicate(x, tmp). There may be other solutions.

Concrete example: see avlja-bug5.c0.txt line 255, and the generated code avlja-bug5.verified.c0.txt, which results in a null pointer exception on line 374.

Workaround: the source program can bind local variables and pass those local variables in as arguments to the function.

[JonathanAldrich]

Confirming that the workaround stated above actually works on the example -- binding local variables for the three rightHeight/leftHeight arguments at line 255.