K-user mailing list

[Manasvi Saxena <manasvi.saxena AT runtimeverification.com>]

The new debugger doesn't have a wiki page yet. The old debugger wiki page can still be used as a guidelines. Most commands are the same. I've been meaning to write a new wiki page, but I probably won't get to it before the weekend. In the meanwhile, I'll be happy to answer all the debugger related questions on the k-list until then.

The debugger can help step through a K Execution. To start a K Debugger Session, run krun with the --debugger flag. The debugger will launch with the initial configuration.

• To take steps, use the step command (step <no. of steps>).
  
• To go back, use the 'back-step' command (b <no.of steps>).
  
• To view the configuration, use the peek command.
  
• To match a pattern on the current configuration, use the "show" command. (show <pattern>)
• To set a watch, use the "watch" command (watch <pattern>). Watches in the K debugger behave similar to most other debuggers. The pattern specified is matched on the configuration after every step/back step command, and the resulting substitution is displayed.
  

There are many other commands, which should be fairly straight forward to figure out in the session itself.

Thanks,

Manasvi

On Wed, Feb 10, 2016 at 6:44 AM, Radoi, Cosmin A <cos AT illinois.edu> wrote:

Manasvi,

Is the debugging functionality you worked on documented somewhere?

Thanks,

Cosmin

> On Feb 9, 2016, at 4:44 PM, davidistreader AT gmail.com wrote:
>
> I have been reading a lot of the papers and am getting a better idea of what
> is going on but lack some basic understanding + what to read to improve.
>
> So any ideas about what to read, particularly  with regard to debugging K
> definitions would be of great help.
>
> Why is the rule I used no a heating rule?  Having made this mistake is there a
> way for me to (a) see the rules build by the kompile  or (b) step through the
> K execution?