Skip to Content.
Sympa Menu

k-user - Re: [[K-user] ] test cases cannot terminate using krun

k-user AT lists.cs.illinois.edu

Subject: K-user mailing list

List archive

Re: [[K-user] ] test cases cannot terminate using krun


Chronological Thread 
  • From: 朱晓冉 <zhuxrsandra AT 163.com>
  • To: "Moore, Brandon Michael" <bmmoore AT illinois.edu>
  • Cc: "k-user AT cs.uiuc.edu" <k-user AT cs.uiuc.edu>
  • Subject: Re: [[K-user] ] test cases cannot terminate using krun
  • Date: Sat, 31 Oct 2015 15:07:18 +0800

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

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




Archive powered by MHonArc 2.6.16.

Top of Page