Skip to content
This repository was archived by the owner on Feb 1, 2020. It is now read-only.

K Debugger

Jump to bottom
Manasvi Saxena edited this page Jan 5, 2015 · 20 revisions

Current Status

Currently K has a textual debugger, which has the following functionality:

  • Stepping - Step by step execution is supported. The initial and subsequent configurations are displayed. User can specify the number of steps that should be taken.

  • Subsequent States - All possible states that can be reached from a particular state. Another state can be selected from these states for further execution.

Future Direction

We need to design two APIs, one for the rewrite engine and one for the debugger itself. Below we define the interfaces corresponding to these APIs. We should refrain from implementing anything in terms of debugging support until we nail down these interfaces.

Rewrite Engine API

This is the API by which the K framework tools make use of the rewrite engine provided by a backend. We want this API to be minimal and efficient. For example, an interface providing only a one-step rewrite relation is minimal but not efficient.

Debugger API

This is the API by which various debugger instances can access the state of the debugger.

Clone this wiki locally