search

team-worthwhile / worthwhile

PSE am KIT 2011/12: Programmverifikation (Team 2)
BSD 3-Clause "New" or "Revised" License
5 stars 3 forks source link

NullPointerException when returning empty array literal #94

Closed jspam closed 12 years ago

jspam commented 12 years ago

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)
bafain commented 12 years ago

The empty array literal's base type, when returned by a function, is not set. I forgot to cover this case when assigning empty array literals a type in 4d905ba123aee9c2ce09572d496e3b44db7a4e7c. Sorry for this and I do not think that the prover has to treat this error.