search

Whiley / WhileyCompiler

The Whiley Compiler (WyC)
http://whiley.org
Apache License 2.0
217 stars 36 forks source link

Bug with Property + Tuple #1128

Closed DavePearce closed 2 years ago

DavePearce commented 2 years ago

The following program exposes a bug:

property inc(int[] xs) -> (int[] r, int q):
    (xs,0)

The error is:

Java output "Exception in thread "main" java.lang.NullPointerException: Cannot invoke "java.lang.Boolean.booleanValue()" because "consumed" is null
    at wyil.transform.MoveAnalysis.visitVariableAccess(MoveAnalysis.java:200)
    at wyil.transform.MoveAnalysis.visitVariableAccess(MoveAnalysis.java:68)
    at wyil.util.AbstractConsumer.visitExpression(AbstractConsumer.java:375)
    at wyil.util.AbstractConsumer.visitExpressions(AbstractConsumer.java:351)
    at wyil.util.AbstractConsumer.visitTupleInitialiser(AbstractConsumer.java:810)
    at wyil.util.AbstractConsumer.visitNaryOperator(AbstractConsumer.java:591)
    at wyil.util.AbstractConsumer.visitExpression(AbstractConsumer.java:427)
    at wyil.util.AbstractConsumer.visitStatement(AbstractConsumer.java:240)
    at wyil.util.AbstractConsumer.visitProperty(AbstractConsumer.java:152)
    at wyil.util.AbstractConsumer.visitCallable(AbstractConsumer.java:126)
    at wyil.util.AbstractConsumer.visitDeclaration(AbstractConsumer.java:65)
    at wyil.util.AbstractConsumer.visitUnit(AbstractConsumer.java:74)
    at wyil.util.AbstractConsumer.visitModule(AbstractConsumer.java:37)
    at wyil.transform.MoveAnalysis.apply(MoveAnalysis.java:72)
    at wyc.task.CompileTask.compile(CompileTask.java:159)
    at wyc.Compiler.run(Compiler.java:144)
    at wyc.Compiler.main(Compiler.java:190)