K-user mailing list

[Gurvan Le Guernic <gleguern AT gmail.com>]

   Hi,

 I have some errors messages with the K debugger. I wrote a simple toy language (park.k3) to show the features of K. It runs well on the simple program attached to this message.

 I was willing to test and show the debugger. However I get an error when I tried:
"[Error] Internal: Uncaught exception thrown of type NoSuchElementException."

 More informations below :

$ kompile --version
K framework version 3.6
Git revision: 28ea17d
Git branch: UNKNOWN
Build date: Fri Aug 21 22:36:54 CEST 2015

$ krun --version
K framework version 3.6
Git revision: 28ea17d
Git branch: UNKNOWN
Build date: Fri Aug 21 22:36:54 CEST 2015

I run :
$ kompile park.k3
$ krun --debugger simple.park

I then get to a prompt: "Command >"

If I type "step 1", I get an help message.

If I type "step -s 1" or "step", I get the error message.

Here is the trace (krun --debug --debugger simple.park):

Command > step
java.util.NoSuchElementException: No value present
    at java.util.Optional.get(Optional.java:135)
    at org.kframework.krun.api.ExecutorDebugger.step(ExecutorDebugger.java:112)
    at org.kframework.krun.tools.Debugger$Tool.run(Debugger.java:266)
    at org.kframework.krun.tools.Debugger$Tool.run(Debugger.java:124)
    at org.kframework.krun.KRunFrontEnd.run(KRunFrontEnd.java:131)
    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.util.NoSuchElementException: No value present
    at java.util.Optional.get(Optional.java:135)
    at org.kframework.krun.api.ExecutorDebugger.step(ExecutorDebugger.java:112)
    at org.kframework.krun.tools.Debugger$Tool.run(Debugger.java:266)
    at org.kframework.krun.tools.Debugger$Tool.run(Debugger.java:124)
    at org.kframework.krun.KRunFrontEnd.run(KRunFrontEnd.java:131)
    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 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

 Do I have a old nonfunctional version of the debugger, or is there a problem ?

   Thanks,

   Gurvan

Attachment: park.k3
Description: Binary data

Attachment: simple.park
Description: Binary data