K-user mailing list

[<daparpon AT dsic.upv.es>]

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