K-user mailing list

["Chen, Xiaohong" <xc3 AT illinois.edu>]

Hi Daniel,

Usually this error message shows up when there is a "requries file.k" in your 
definition but "file.k" does not exist. Please double check that you setup 
all environment variables correctly, especially LD_LIBRARY_PATH. If that does 
not solve the problem, could you please provide more information specially so 
that we can help nail down the problem? 

Also we are improving this error message, too.

Thanks,
Xiaohong

-------------------------
Chen, Xiaohong
BSc, Peking University
PhD student, UIUC

________________________________________
From: 
daparpon AT dsic.upv.es
 
[daparpon AT dsic.upv.es]
Sent: Thursday, July 27, 2017 5:31 AM
To: 
k-user AT lists.cs.illinois.edu
Subject: [[K-user] ] Error when compiling sample Kernel-C specification

Hi! I am interested in trying out the K 4.0 verification infrastructure to
learn about how it works and how I can integrate it within my project.
However, when I try to compile the Kernel-C specification provided in k/
samples/kernelc, I get the following error message:

"[Error] Internal: Uncaught exception thrown of type NoSuchElementException.
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";

Following the suggestion, I ran kompile again with the --debug flag, and in
return I got the description below:

"java.util.NoSuchElementException: No value present
        at java.util.Optional.get(Optional.java:135)
        at
org.kframework.parser.concrete2kore.ParserUtils.slurp(ParserUtils.java:152)
        at
org.kframework.parser.concrete2kore.ParserUtils.slurp(ParserUtils.java:119)
        at
org.kframework.parser.concrete2kore.ParserUtils.loadModules(ParserUtils.java:207)
        at
org.kframework.parser.concrete2kore.ParserUtils.loadDefinition(ParserUtils.java:254)
        at
org.kframework.kompile.DefinitionParsing.parseDefinition(DefinitionParsing.java:169)
        at
org.kframework.kompile.DefinitionParsing.parseDefinitionAndResolveBubbles(DefinitionParsing.java:153)
        at
org.kframework.kompile.DefinitionParsing.parseDefinitionAndResolveBubbles(DefinitionParsing.java:149)
        at org.kframework.kompile.Kompile.parseDefinition(Kompile.java:140)
        at org.kframework.kompile.KompileFrontEnd.run(KompileFrontEnd.java:54)
        at org.kframework.main.FrontEnd.main(FrontEnd.java:34)
        at org.kframework.main.Main.runApplication(Main.java:415)
        at org.kframework.main.Main.runApplication(Main.java:131)
        at org.kframework.main.Main.main(Main.java:73)"

In fact, this last exception message is printed twice. What can I do to solve
this problem and compile the specification?

Thanks in advance,
Daniel