team-worthwhile/worthwhile — Issue #93: NullPointerException on loop after return statement
Author: jspam
Created: 2012-02-22 15:59:21+00:00
State: open
Labels: prover

Try to prove the following program:

```
function Integer noop(Integer a)
_ensures _return = a
{
return a

while (false)
_invariant true
{

}
}
```

The following exception is thrown:

```
java.lang.NullPointerException
at edu.kit.iti.formal.pse.worthwhile.prover.FreshVariableSetVisitor.visit(FreshVariableSetVisitor.java:115)
at edu.kit.iti.formal.pse.worthwhile.model.ast.visitor.HierarchialASTNodeVisitor.visit(HierarchialASTNodeVisitor.java:343)
at edu.kit.iti.formal.pse.worthwhile.model.ast.ReturnValueReference.accept(ReturnValueReference.java:48)
at edu.kit.iti.formal.pse.worthwhile.prover.FreshVariableSetVisitor.visit(FreshVariableSetVisitor.java:71)
at edu.kit.iti.formal.pse.worthwhile.model.ast.visitor.HierarchialASTNodeVisitor.visit(HierarchialASTNodeVisitor.java:163)
at edu.kit.iti.formal.pse.worthwhile.model.ast.Equal.accept(Equal.java:47)
at edu.kit.iti.formal.pse.worthwhile.prover.FreshVariableSetVisitor.visit(FreshVariableSetVisitor.java:72)
at edu.kit.iti.formal.pse.worthwhile.model.ast.visitor.HierarchialASTNodeVisitor.visit(HierarchialASTNodeVisitor.java:208)
at edu.kit.iti.formal.pse.worthwhile.model.ast.Implication.accept(Implication.java:47)
at edu.kit.iti.formal.pse.worthwhile.prover.WPStrategy.visit(WPStrategy.java:402)
at edu.kit.iti.formal.pse.worthwhile.model.ast.Loop.accept(Loop.java:235)
at edu.kit.iti.formal.pse.worthwhile.prover.WPStrategy.visit(WPStrategy.java:165)
at edu.kit.iti.formal.pse.worthwhile.model.ast.Block.accept(Block.java:92)
at edu.kit.iti.formal.pse.worthwhile.prover.WPStrategy.visit(WPStrategy.java:295)
at edu.kit.iti.formal.pse.worthwhile.model.ast.FunctionDeclaration.accept(FunctionDeclaration.java:356)
at edu.kit.iti.formal.pse.worthwhile.prover.WPStrategy.visit(WPStrategy.java:441)
at edu.kit.iti.formal.pse.worthwhile.model.ast.Program.accept(Program.java:197)
at edu.kit.iti.formal.pse.worthwhile.prover.WPStrategy.transformProgram(WPStrategy.java:65)
at edu.kit.iti.formal.pse.worthwhile.prover.SpecificationChecker.checkProgram(SpecificationChecker.java:329)
at edu.kit.iti.formal.pse.worthwhile.ui.proving.WorthwhileProveJob.run(WorthwhileProveJob.java:80)
at org.eclipse.core.internal.jobs.Worker.run(Worker.java:54)
```

When the loop is removed, the exception is not thrown.