A method that has an obligation to terminate is allowed to call a non-terminating method as shown in the following example:
#!chalice
class A {
method test_false_postcondition()
ensures false;
{
while (true) {}
}
method test_false_postcondition_caller()
requires mustTerminate(2);
{
//:: ExpectedOutput(assert.failed:assertion.false)
//:: MissingOutput(assert.failed:assertion.false, /Chalice2Silver/issue/84/)
call test_false_postcondition();
assert false;
}
}
The problem is that the encoding checks if called method picked the obligation to terminate after the call. However, if method's postcondition is false, then this check trivially succeeds.
A method that has an obligation to terminate is allowed to call a non-terminating method as shown in the following example:
The problem is that the encoding checks if called method picked the obligation to terminate after the call. However, if method's postcondition is
false, then this check trivially succeeds.