K-user mailing list

[朱晓冉 <zhuxrsandra AT 163.com>]

Hi,

Thank you for your reply.

I have found the reason of this problem. Since there is no terminate state of my program, I have changed the infinite loop into a finite one of the program and it can run correctly now.

 Bests,

Xiaoran Zhu

?? 2015??10??30????????3:31??Moore, Brandon Michael <bmmoore AT illinois.edu> ??????

Hello.

Thank you for trying K.

There is clearly a problem in K for it to be failing with such an exception.
Even if there is a problem in your file you should get a better error message.

Can you shoud us what program you are trying to kompile or run?

Brandon

---

From: ?????? [zhuxrsandra AT 163.com]
Sent: Sunday, October 25, 2015 8:40 AM
To: Rosu, Grigore
Cc: k-user AT cs.uiuc.edu
Subject: Re: [[K-user] ] test cases cannot terminate using krun

The version of K that I am using is 3.5. 

I downloaded K 3.6 just now and tried to compile my project. But some error occurs as follows:

java.lang.NullPointerException

at org.kframework.kil.AbstractVisitor.visitNode(AbstractVisitor.java:103)

at org.kframework.backend.java.symbolic.KILtoBackendJavaKILTransformer.visit(KILtoBackendJavaKILTransformer.java:496)

at org.kframework.backend.java.symbolic.KILtoBackendJavaKILTransformer.visit(KILtoBackendJavaKILTransformer.java:74)

at org.kframework.kil.Rule.accept(Rule.java:64)

at org.kframework.kil.AbstractVisitor.visitNode(AbstractVisitor.java:103)

at org.kframework.backend.java.symbolic.KILtoBackendJavaKILTransformer.visit(KILtoBackendJavaKILTransformer.java:563)

at org.kframework.backend.java.symbolic.KILtoBackendJavaKILTransformer.visit(KILtoBackendJavaKILTransformer.java:74)

at org.kframework.kil.Definition.accept(Definition.java:154)

at org.kframework.kil.AbstractVisitor.visitNode(AbstractVisitor.java:103)

at org.kframework.backend.java.symbolic.KILtoBackendJavaKILTransformer.transformDefinition(KILtoBackendJavaKILTransformer.java:107)

at org.kframework.backend.java.symbolic.JavaSymbolicBackend.lastStep(JavaSymbolicBackend.java:76)

at org.kframework.backend.LastStep.compile(LastStep.java:21)

at org.kframework.backend.LastStep.compile(LastStep.java:10)

at org.kframework.compile.utils.CompilerSteps.compile(CompilerSteps.java:44)

at org.kframework.kompile.KompileFrontEnd.genericCompile(KompileFrontEnd.java:130)

at org.kframework.kompile.KompileFrontEnd.run(KompileFrontEnd.java:97)

at org.kframework.main.FrontEnd.main(FrontEnd.java:52)

at org.kframework.main.Main.runApplication(Main.java:109)

at org.kframework.main.Main.runApplication(Main.java:99)

at org.kframework.main.Main.main(Main.java:51)

java.lang.NullPointerException

at org.kframework.kil.AbstractVisitor.visitNode(AbstractVisitor.java:103)

at org.kframework.backend.java.symbolic.KILtoBackendJavaKILTransformer.visit(KILtoBackendJavaKILTransformer.java:496)

at org.kframework.backend.java.symbolic.KILtoBackendJavaKILTransformer.visit(KILtoBackendJavaKILTransformer.java:74)

at org.kframework.kil.Rule.accept(Rule.java:64)

at org.kframework.kil.AbstractVisitor.visitNode(AbstractVisitor.java:103)

at org.kframework.backend.java.symbolic.KILtoBackendJavaKILTransformer.visit(KILtoBackendJavaKILTransformer.java:563)

at org.kframework.backend.java.symbolic.KILtoBackendJavaKILTransformer.visit(KILtoBackendJavaKILTransformer.java:74)

at org.kframework.kil.Definition.accept(Definition.java:154)

at org.kframework.kil.AbstractVisitor.visitNode(AbstractVisitor.java:103)

at org.kframework.backend.java.symbolic.KILtoBackendJavaKILTransformer.transformDefinition(KILtoBackendJavaKILTransformer.java:107)

at org.kframework.backend.java.symbolic.JavaSymbolicBackend.lastStep(JavaSymbolicBackend.java:76)

at org.kframework.backend.LastStep.compile(LastStep.java:21)

at org.kframework.backend.LastStep.compile(LastStep.java:10)

at org.kframework.compile.utils.CompilerSteps.compile(CompilerSteps.java:44)

at org.kframework.kompile.KompileFrontEnd.genericCompile(KompileFrontEnd.java:130)

at org.kframework.kompile.KompileFrontEnd.run(KompileFrontEnd.java:97)

at org.kframework.main.FrontEnd.main(FrontEnd.java:52)

at org.kframework.main.Main.runApplication(Main.java:109)

at org.kframework.main.Main.runApplication(Main.java:99)

at org.kframework.main.Main.main(Main.java:51)

[Error] Internal: Uncaught exception thrown of type NullPointerException.

Please rerun your program with the --debug flag to generate a stack trace, and

file a bug report at https://github.com/kframework/k/issues

Need I do some changes in my project while using K 3.6 or are there anything wrong about the project?

Thanks!

Xiaoran Zhu

?? 2015??10??25????????8:34??Rosu, Grigore <grosu AT illinois.edu> ??????

Can you please tell us what version of K are you using?  We recommend using the stable, K 3.6 version for now, because we are making heavy changes in the current code base in order to release K 4.0.

Grigore

 

 

---

From: ?????? [zhuxrsandra AT 163.com]
Sent: Sunday, October 25, 2015 7:19 AM
To: k-user AT cs.uiuc.edu
Subject: [[K-user] ] test cases cannot terminate using krun

Hi,

I wonder why a program may not run successfully. When I test my project written in K, some of my test cases cannot run successfully, i.e. when inputting the command ??krun test ??search??, nothing outputs and it seems that this program cannot terminate. 

I have found which rules lead to this condition. But it seems there is no syntax error or semantic error in these rules.

Are there any possible reasons that may result in this problem?

Many thanks!

Bests,

Xiaoran Zhu