Return value is not passed on to the prover in postconditions.

[jspam]

See testIndexedReturnVariableReference in InterpreterAstNodeVisitorTest, following test program:

function Integer[] test2(Integer N, Integer[] a)
  _ensures forall Integer i, 0 <= i && i < N : _return[i] ≥ 0
{
  return a
}

Integer[] test := test2(6, {6, 4, 2, 3, 5, 1})

This test fails with an unknown validity interpreter error.

Debugging in InterpreterAstNodeVisitor::getAllSymbols(), one can see that the variable symbolStack is defined as follows:

[{edu.kit.iti.formal.pse.worthwhile.model.ast.VariableDeclaration@56fb2ac4 (name: a)=edu.kit.iti.formal.pse.worthwhile.model.CompositeValue@15, edu.kit.iti.formal.pse.worthwhile.model.ast.VariableDeclaration@ba3bff5 (name: N)=edu.kit.iti.formal.pse.worthwhile.model.IntegerValue@6}, {}]

This means that only the variables a and N are visible in the context of the postcondition, but not the return variable reference, so the return variable reference is not passed on to the prover, which promptly fails to evaluate the quantified expression.

[jspam]

How can you close this issue when the test I wrote for it still fails? This time it is because you didn’t set the type of the _return variable declaration (which, I think, should be the same type as the function’s return type)

[FRONDS]

Because the test fails also because the prover doesn't use the _return variable yet, and I wanted to work on other issues, so I had to commit.

[jspam]

You can commit without marking the issue as fixed by just writing "#61" somewhere in the commit message. That way the commit will be mentioned here without the issue being closed.

[jspam]

The base type of the array type is not set, see note on 1fb1df6#L0R1148 line 1148

[jspam]

Fixed in e1f9c3a, for some reason GitHub is not displaying this.