k-user AT lists.cs.illinois.edu

Subject: K-user mailing list

List archive

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

From: 朱晓冉 <zhuxrsandra AT 163.com>
To: "Rosu, Grigore" <grosu 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: Sun, 25 Oct 2015 21:40:26 +0800

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

[[K-user] ] test cases cannot terminate using krun, 朱晓冉, 10/25/2015
- RE: [[K-user] ] test cases cannot terminate using krun, Rosu, Grigore, 10/25/2015
  - Re: [[K-user] ] test cases cannot terminate using krun, 朱晓冉, 10/25/2015
    - RE: [[K-user] ] test cases cannot terminate using krun, Moore, Brandon Michael, 10/29/2015
      - Re: [[K-user] ] test cases cannot terminate using krun, 朱晓冉, 10/31/2015