team-worthwhile/worthwhile — Issue #94: NullPointerException when returning empty array literal
Author: jspam
Created: 2012-02-23 15:23:28+00:00
State: open
Labels: prover

Trying to prove the following program:

```
function Integer[] test() {
return {}
}
```

causes the following exception:

```
!MESSAGE An internal error occurred during: "Prove Temp.ww".
!STACK 0
java.lang.NullPointerException
at edu.kit.iti.formal.pse.worthwhile.model.ast.visitor.ASTNodeReturnVisitor.apply(ASTNodeReturnVisitor.java:46)
at edu.kit.iti.formal.pse.worthwhile.prover.ArrayFunctionInserter.visit(ArrayFunctionInserter.java:62)
at edu.kit.iti.formal.pse.worthwhile.model.ast.ArrayLiteral.accept(ArrayLiteral.java:92)
at edu.kit.iti.formal.pse.worthwhile.prover.SubstitutionVisitor.visit(SubstitutionVisitor.java:261)
at edu.kit.iti.formal.pse.worthwhile.prover.ArrayFunctionInserter.visit(ArrayFunctionInserter.java:1)
at edu.kit.iti.formal.pse.worthwhile.model.ast.ReturnStatement.accept(ReturnStatement.java:128)
at edu.kit.iti.formal.pse.worthwhile.prover.SubstitutionVisitor.visit(SubstitutionVisitor.java:223)
at edu.kit.iti.formal.pse.worthwhile.prover.ArrayFunctionInserter.visit(ArrayFunctionInserter.java:1)
at edu.kit.iti.formal.pse.worthwhile.model.ast.Block.accept(Block.java:92)
at edu.kit.iti.formal.pse.worthwhile.prover.SubstitutionVisitor.visit(SubstitutionVisitor.java:141)
at edu.kit.iti.formal.pse.worthwhile.prover.ArrayFunctionInserter.visit(ArrayFunctionInserter.java:1)
at edu.kit.iti.formal.pse.worthwhile.model.ast.FunctionDeclaration.accept(FunctionDeclaration.java:356)
at edu.kit.iti.formal.pse.worthwhile.prover.SubstitutionVisitor.visit(SubstitutionVisitor.java:127)
at edu.kit.iti.formal.pse.worthwhile.prover.ArrayFunctionInserter.visit(ArrayFunctionInserter.java:1)
at edu.kit.iti.formal.pse.worthwhile.model.ast.Program.accept(Program.java:197)
at edu.kit.iti.formal.pse.worthwhile.prover.SpecificationChecker.checkProgram(SpecificationChecker.java:326)
at edu.kit.iti.formal.pse.worthwhile.ui.proving.WorthwhileProveJob.run(WorthwhileProveJob.java:81)
at org.eclipse.core.internal.jobs.Worker.run(Worker.java:54)
```