search

LayerXcom / verified-vyper-contracts

FVyper: A collection of useful Vyper contracts developed with formal methods
Apache License 2.0
55 stars 15 forks source link

Update K and KEVM #20

Closed nrryuya closed 5 years ago

nrryuya commented 5 years ago 
java.lang.NullPointerException
    at org.kframework.backend.java.kil.KItem.toString(KItem.java:823)
    at com.google.common.base.Joiner.toString(Joiner.java:434)
    at com.google.common.base.Joiner.appendTo(Joiner.java:111)
    at com.google.common.base.Joiner.appendTo(Joiner.java:152)
    at com.google.common.base.Joiner.appendTo(Joiner.java:140)
    at org.kframework.backend.java.kil.KCollection.toString(KCollection.java:86)
    at org.kframework.backend.java.kil.KItem.toStringImpl(KItem.java:843)
    at org.kframework.backend.java.kil.KItem.toString(KItem.java:822)
    at com.google.common.base.Joiner.toString(Joiner.java:434)
    at com.google.common.base.Joiner.appendTo(Joiner.java:111)
    at com.google.common.base.Joiner.appendTo(Joiner.java:152)
    at com.google.common.base.Joiner.appendTo(Joiner.java:140)
    at org.kframework.backend.java.kil.KCollection.toString(KCollection.java:86)
    at org.kframework.backend.java.kil.KItem.toStringImpl(KItem.java:843)
    at org.kframework.backend.java.kil.KItem.toString(KItem.java:822)
    at com.google.common.base.Joiner.toString(Joiner.java:434)
    at com.google.common.base.Joiner.appendTo(Joiner.java:111)
    at com.google.common.base.Joiner.appendTo(Joiner.java:152)
    at com.google.common.base.Joiner.appendTo(Joiner.java:140)
    at org.kframework.backend.java.kil.KCollection.toString(KCollection.java:86)
    at org.kframework.backend.java.kil.KItem.toStringImpl(KItem.java:843)
    at org.kframework.backend.java.kil.KItem.toString(KItem.java:822)
    at com.google.common.base.Joiner.toString(Joiner.java:434)
    at com.google.common.base.Joiner.appendTo(Joiner.java:111)
    at com.google.common.base.Joiner.appendTo(Joiner.java:152)
    at com.google.common.base.Joiner.appendTo(Joiner.java:140)
    at org.kframework.backend.java.kil.KCollection.toString(KCollection.java:86)
    at org.kframework.backend.java.kil.KItem.toStringImpl(KItem.java:843)
    at org.kframework.backend.java.kil.KItem.toString(KItem.java:822)
    at com.google.common.base.Joiner.toString(Joiner.java:434)
    at com.google.common.base.Joiner.appendTo(Joiner.java:111)
    at com.google.common.base.Joiner.appendTo(Joiner.java:152)
    at com.google.common.base.Joiner.appendTo(Joiner.java:140)
    at org.kframework.backend.java.kil.KCollection.toString(KCollection.java:86)
    at org.kframework.backend.java.kil.KItem.toStringImpl(KItem.java:843)
    at org.kframework.backend.java.kil.KItem.toString(KItem.java:822)
    at com.google.common.base.Joiner.toString(Joiner.java:434)
    at com.google.common.base.Joiner.appendTo(Joiner.java:111)
    at com.google.common.base.Joiner.appendTo(Joiner.java:152)
    at com.google.common.base.Joiner.appendTo(Joiner.java:140)
    at org.kframework.backend.java.kil.KCollection.toString(KCollection.java:86)
    at org.kframework.backend.java.kil.KItem.toStringImpl(KItem.java:843)
    at org.kframework.backend.java.kil.KItem.toString(KItem.java:822)
    at com.google.common.base.Joiner.toString(Joiner.java:434)
    at com.google.common.base.Joiner.appendTo(Joiner.java:111)
    at com.google.common.base.Joiner.appendTo(Joiner.java:152)
    at com.google.common.base.Joiner.appendTo(Joiner.java:140)
    at org.kframework.backend.java.kil.KCollection.toString(KCollection.java:86)
    at org.kframework.backend.java.kil.KItem.toStringImpl(KItem.java:843)
    at org.kframework.backend.java.kil.KItem.toString(KItem.java:822)
    at com.google.common.base.Joiner.toString(Joiner.java:434)
    at com.google.common.base.Joiner.appendTo(Joiner.java:111)
    at com.google.common.base.Joiner.appendTo(Joiner.java:152)
    at com.google.common.base.Joiner.appendTo(Joiner.java:140)
    at org.kframework.backend.java.kil.KCollection.toString(KCollection.java:86)
    at org.kframework.backend.java.kil.KItem.toStringImpl(KItem.java:843)
    at org.kframework.backend.java.kil.KItem.toString(KItem.java:822)
    at com.google.common.base.Joiner.toString(Joiner.java:434)
    at com.google.common.base.Joiner.appendTo(Joiner.java:111)
    at com.google.common.base.Joiner.appendTo(Joiner.java:152)
    at com.google.common.base.Joiner.appendTo(Joiner.java:140)
    at org.kframework.backend.java.kil.KCollection.toString(KCollection.java:86)
    at org.kframework.backend.java.kil.KItem.toStringImpl(KItem.java:843)
    at org.kframework.backend.java.kil.KItem.toString(KItem.java:822)
    at com.google.common.base.Joiner.toString(Joiner.java:434)
    at com.google.common.base.Joiner.appendTo(Joiner.java:111)
    at com.google.common.base.Joiner.appendTo(Joiner.java:152)
    at com.google.common.base.Joiner.appendTo(Joiner.java:140)
    at org.kframework.backend.java.kil.KCollection.toString(KCollection.java:86)
    at org.kframework.backend.java.kil.KItem.toStringImpl(KItem.java:843)
    at org.kframework.backend.java.kil.KItem.toString(KItem.java:822)
    at com.google.common.base.Joiner.toString(Joiner.java:434)
    at com.google.common.base.Joiner.appendTo(Joiner.java:111)
    at com.google.common.base.Joiner.appendTo(Joiner.java:152)
    at com.google.common.base.Joiner.appendTo(Joiner.java:140)
    at org.kframework.backend.java.kil.KCollection.toString(KCollection.java:86)
    at org.kframework.backend.java.kil.KItem.toStringImpl(KItem.java:843)
    at org.kframework.backend.java.kil.KItem.toString(KItem.java:822)
    at com.google.common.base.Joiner.toString(Joiner.java:434)
    at com.google.common.base.Joiner.appendTo(Joiner.java:111)
    at com.google.common.base.Joiner.appendTo(Joiner.java:152)
    at com.google.common.base.Joiner.appendTo(Joiner.java:140)
    at org.kframework.backend.java.kil.KCollection.toString(KCollection.java:86)
    at org.kframework.backend.java.kil.KItem.toStringImpl(KItem.java:843)
    at org.kframework.backend.java.kil.KItem.toString(KItem.java:822)
    at org.kframework.backend.java.symbolic.ConjunctiveFormula.toString(ConjunctiveFormula.java:1043)
    at org.kframework.backend.java.symbolic.SymbolicRewriter.proveRule(SymbolicRewriter.java:742)
    at org.kframework.backend.java.symbolic.InitializeRewriter$SymbolicRewriterGlue.lambda$prove$2(InitializeRewriter.java:237)
    at java.util.stream.ReferencePipeline$3$1.accept(ReferencePipeline.java:193)
    at java.util.stream.ReferencePipeline$2$1.accept(ReferencePipeline.java:175)
    at java.util.ArrayList$ArrayListSpliterator.forEachRemaining(ArrayList.java:1374)
    at java.util.stream.AbstractPipeline.copyInto(AbstractPipeline.java:481)
    at java.util.stream.AbstractPipeline.wrapAndCopyInto(AbstractPipeline.java:471)
    at java.util.stream.ReduceOps$ReduceOp.evaluateSequential(ReduceOps.java:708)
    at java.util.stream.AbstractPipeline.evaluate(AbstractPipeline.java:234)
    at java.util.stream.ReferencePipeline.collect(ReferencePipeline.java:499)
    at org.kframework.backend.java.symbolic.InitializeRewriter$SymbolicRewriterGlue.prove(InitializeRewriter.java:240)
    at org.kframework.kprove.KProve.run(KProve.java:68)
    at org.kframework.kprove.KProveFrontEnd.run(KProveFrontEnd.java:96)
    at org.kframework.main.FrontEnd.main(FrontEnd.java:52)
    at org.kframework.main.Main.runApplication(Main.java:118)
    at org.kframework.main.Main.runApplication(Main.java:107)
    at org.kframework.main.Main.main(Main.java:53)