team-worthwhile/worthwhile — Issue #95: NullPointerException in test_fibonacci.ww during interpreter run
Author: jspam
Created: 2012-02-24 00:25:09+00:00
State: open
Labels: prover

(Assuming this deserves the label `prover` since the exception occurs in `SMTLIBStrategy`)

The file `test_fibonacci.ww` can now be proven correct (hooray!), but when executing it in the interpreter, the third postcondition fails to validate and produces an "Unknown validity" interpreter error.

When you insert `e.printStackTrace();` in `SpecificationChecker.java` after line 313 (when the exception from the prover is caught), you'll see that the cause is an exception with the stack trace attached below. The culprit is the following line in `SMTLIBStrategy.java`:

```
String varrefString = variableReference.getVariable().getName();
```

which does not play too well with our old friend `_return` (as debugging in that method shows).

```
java.lang.NullPointerException
at java.util.concurrent.FutureTask$Sync.innerGet(FutureTask.java:262)
at java.util.concurrent.FutureTask.get(FutureTask.java:119)
at edu.kit.iti.formal.pse.worthwhile.prover.SpecificationChecker.getValidity(SpecificationChecker.java:304)
at edu.kit.iti.formal.pse.worthwhile.prover.SpecificationChecker.checkProgram(SpecificationChecker.java:366)
at edu.kit.iti.formal.pse.worthwhile.prover.SpecificationChecker.checkFormula(SpecificationChecker.java:274)
at edu.kit.iti.formal.pse.worthwhile.prover.SpecificationChecker.checkFormula(SpecificationChecker.java:196)
at edu.kit.iti.formal.pse.worthwhile.interpreter.InterpreterASTNodeVisitor.visit(InterpreterASTNodeVisitor.java:1118)
at edu.kit.iti.formal.pse.worthwhile.model.ast.visitor.HierarchialASTNodeVisitor.visit(HierarchialASTNodeVisitor.java:201)
at edu.kit.iti.formal.pse.worthwhile.model.ast.ForAllQuantifier.accept(ForAllQuantifier.java:48)
at edu.kit.iti.formal.pse.worthwhile.interpreter.InterpreterASTNodeVisitor.visitAnnotation(InterpreterASTNodeVisitor.java:476)
at edu.kit.iti.formal.pse.worthwhile.interpreter.InterpreterASTNodeVisitor.visit(InterpreterASTNodeVisitor.java:1071)
at edu.kit.iti.formal.pse.worthwhile.model.ast.Postcondition.accept(Postcondition.java:47)
at edu.kit.iti.formal.pse.worthwhile.interpreter.InterpreterASTNodeVisitor.visit(InterpreterASTNodeVisitor.java:815)
at edu.kit.iti.formal.pse.worthwhile.model.ast.FunctionDeclaration.accept(FunctionDeclaration.java:356)
at edu.kit.iti.formal.pse.worthwhile.interpreter.InterpreterASTNodeVisitor.visit(InterpreterASTNodeVisitor.java:784)
at edu.kit.iti.formal.pse.worthwhile.model.ast.FunctionCall.accept(FunctionCall.java:155)
at edu.kit.iti.formal.pse.worthwhile.interpreter.InterpreterASTNodeVisitor.visit(InterpreterASTNodeVisitor.java:1219)
at edu.kit.iti.formal.pse.worthwhile.model.ast.VariableDeclaration.accept(VariableDeclaration.java:255)
at edu.kit.iti.formal.pse.worthwhile.interpreter.InterpreterASTNodeVisitor.visit(InterpreterASTNodeVisitor.java:612)
at edu.kit.iti.formal.pse.worthwhile.model.ast.Block.accept(Block.java:92)
at edu.kit.iti.formal.pse.worthwhile.interpreter.InterpreterASTNodeVisitor.visit(InterpreterASTNodeVisitor.java:1101)
at edu.kit.iti.formal.pse.worthwhile.model.ast.Program.accept(Program.java:197)
at edu.kit.iti.formal.pse.worthwhile.interpreter.Interpreter.execute(Interpreter.java:93)
at edu.kit.iti.formal.pse.worthwhile.debugger.model.InterpreterRunner.run(InterpreterRunner.java:40)
Caused by: java.lang.NullPointerException
at edu.kit.iti.formal.pse.worthwhile.prover.SMTLIBStrategy.visit(SMTLIBStrategy.java:350)
at edu.kit.iti.formal.pse.worthwhile.model.ast.visitor.HierarchialASTNodeVisitor.visit(HierarchialASTNodeVisitor.java:361)
at edu.kit.iti.formal.pse.worthwhile.model.ast.ReturnValueReference.accept(ReturnValueReference.java:48)
at edu.kit.iti.formal.pse.worthwhile.prover.SMTLIBStrategy.pushBinaryOperation(SMTLIBStrategy.java:91)
at edu.kit.iti.formal.pse.worthwhile.prover.SMTLIBStrategy.visit(SMTLIBStrategy.java:263)
at edu.kit.iti.formal.pse.worthwhile.model.ast.Equal.accept(Equal.java:47)
at edu.kit.iti.formal.pse.worthwhile.prover.SMTLIBStrategy.pushQuantifier(SMTLIBStrategy.java:136)
at edu.kit.iti.formal.pse.worthwhile.prover.SMTLIBStrategy.visit(SMTLIBStrategy.java:278)
at edu.kit.iti.formal.pse.worthwhile.model.ast.ForAllQuantifier.accept(ForAllQuantifier.java:48)
at edu.kit.iti.formal.pse.worthwhile.prover.SMTLIBStrategy.pushBinaryOperation(SMTLIBStrategy.java:92)
at edu.kit.iti.formal.pse.worthwhile.prover.SMTLIBStrategy.visit(SMTLIBStrategy.java:301)
at edu.kit.iti.formal.pse.worthwhile.model.ast.Implication.accept(Implication.java:47)
at edu.kit.iti.formal.pse.worthwhile.prover.SMTLIBStrategy.pushBinaryOperation(SMTLIBStrategy.java:92)
at edu.kit.iti.formal.pse.worthwhile.prover.SMTLIBStrategy.visit(SMTLIBStrategy.java:248)
at edu.kit.iti.formal.pse.worthwhile.model.ast.Conjunction.accept(Conjunction.java:47)
at edu.kit.iti.formal.pse.worthwhile.prover.SMTLIBStrategy.pushUnaryOperation(SMTLIBStrategy.java:107)
at edu.kit.iti.formal.pse.worthwhile.prover.SMTLIBStrategy.visit(SMTLIBStrategy.java:345)
at edu.kit.iti.formal.pse.worthwhile.model.ast.Negation.accept(Negation.java:47)
at edu.kit.iti.formal.pse.worthwhile.prover.SMTLIBStrategy.compileFormula(SMTLIBStrategy.java:60)
at edu.kit.iti.formal.pse.worthwhile.prover.StdProver.checkFormula(StdProver.java:63)
at edu.kit.iti.formal.pse.worthwhile.prover.Z3Prover.checkFormula(Z3Prover.java:1)
at edu.kit.iti.formal.pse.worthwhile.prover.SpecificationChecker$1ProverCallerTask.call(SpecificationChecker.java:297)
at edu.kit.iti.formal.pse.worthwhile.prover.SpecificationChecker$1ProverCallerTask.call(SpecificationChecker.java:1)
at java.util.concurrent.FutureTask$Sync.innerRun(FutureTask.java:334)
at java.util.concurrent.FutureTask.run(FutureTask.java:166)
at java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1110)
at java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:603)
at java.lang.Thread.run(Thread.java:679)
```