Method invocations inside while loop conditions

[Naum-Tomov]

Currently, you cannot use the post-conditions of methods that are invoked inside of while-loop conditions, because they get rewritten into

res =[invocation]
while (res...)

And you cannot use the post-conditions of the invocation, inside the while condition, since it is not preserved inside the res. This warrants some discussion on whether we want to find a way to preserve the post-conditions in these cases and how this can be done.

[Naum-Tomov]

To concretize the problem it has been reduced to the following example:

class Test {
	Test inner;

	context Perm(inner, 1\2);
	ensures \result == inner;
	Test get() {
		return inner;
	}

	context Perm(inner, 1\2);
	void use() {
		loop_invariant Perm(inner, 1\2);
		while(get() != null) {
			assert inner != null;
		}
	}
}

The assertion fails to verify, despite the fact that logically, if you enter the while body, this statement is necessarily true.

The problem here is tied to the way loops are encoded. Further investigation in frama.c with the following example:

int N;
//@  ensures N==0;
int ensuresNis0() {
    N=0;
    return 1;
}

int main() {
    while(ensuresNis0()){
    	//@ assert N==0;
    	int a = 42;
    }
    return 1;
}

In Frama-C this verifies correctly, because the loop gets encoded into:

while (1) {
    int tmp;
    tmp = ensuresNis0();
    if (! tmp) {
      break;
    }
    {
      /*@ assert N ≡ 0; */ ;
      int a = 42;
    }
  }

[bobismijnnaam]

I don't think there is anything in particular preventing us from using frama-c's encoding. We could consider only applying this encoding for impure loop conditions. Are there any downsides I am not seeing?

[pieter-bos]

Implemented here: #932

Indeed only for impure conditions, mostly for readability.