debugging

cfamily.Frame.inside

def Frame.inside {L : Constructs} (k : List (Frame L)) : Bool

Whether the frames are inside a statement already stopped at (its parts) or a loop condition’s preparation, in the same call.

cfamily.Configuration.nextNode

def Configuration.nextNode {L : Constructs} (stops : NodeId -> Bool) (x : Configuration L) : Option NodeId

The node a configuration stops at: its next statement’s, if it is one to stop at (stops: a node the program wrote, not one of the code a dialect generated or a library’s).

cfamily.Frame.callDepth

def Frame.callDepth {L : Constructs} (k : List (Frame L)) : Nat

How many calls deep the frames are.

cfamily.Configuration.depth

def Configuration.depth {L : Constructs} (x : Configuration L) : Nat

How many calls deep a configuration is.

cfamily.Configuration.scanReachesEnd

def Configuration.scanReachesEnd {L : Constructs} (d : RunDialect L) (s : State L) (format : String) (targets : List (TypedExpr L)) : Bool

Whether a scanf would read to the end of the input given so far (more input could change what it reads).

cfamily.Configuration.scanCallReachesEnd

def Configuration.scanCallReachesEnd {L : Constructs} (d : RunDialect L) (s : State L) (args : List (TypedExpr L)) : Bool

Whether a call of scanf in the state s (its format and targets the arguments args, evaluated by the dialect d) would read to the end of the input given so far.

cfamily.Debug.hasNewline

def Debug.hasNewline (cs : List Char) : Bool

Whether the codes have a newline.

cfamily.Configuration.needsInput

def Configuration.needsInput {L : Constructs} (d : RunDialect L) (x : Configuration L) : Bool

Whether the next statement reads input that may not all be there yet: scanf reaching the end, getchar with no input, fgets with no newline, a dialect’s statement that says so.

cfamily.Configuration.state

def Configuration.state {L : Constructs} (x : Configuration L) : Option (State L)

The state of a configuration, if it has one.

cfamily.Configuration.noteCount

def Configuration.noteCount {L : Constructs} (x : Configuration L) : Nat

How many divergences a configuration has noted (an assumed choice is not one).

cfamily.ReasonDescription.kindOf

def ReasonDescription.kindOf (r : ReasonDescription) : ReasonKind

A reason’s kind.

cfamily.Dialect.halt

def Dialect.halt {L : Constructs} (d : Dialect L) (x : Configuration L) (y : Configuration L) : Option (Halt (Stopped L) (State L) (Stopped L) (Outcome L))

How a finished run ends for the debugger: a stop’s kind by its reason (the state before the move that stopped).

cfamily.Dialect.machine

def Dialect.machine {L : Constructs} (d : Dialect L) (c : CheckedProgram L) (stops : NodeId -> Bool) : Machine (Configuration L) Unit (Stopped L) (State L) (Stopped L) (Outcome L)

The C family’s machine for the debugger driver, for a checked program, stopping at the nodes stops says.

cfamily.Dialect.reasonJson

def Dialect.reasonJson {L : Constructs} (d : Dialect L) (w : Stopped L) : Json

A stop’s reason as the host reads it: {kind, pre, clause, values, op}.

cfamily.Dialect.noteJson

def Dialect.noteJson {L : Constructs} (d : Dialect L) (w : Stopped L) : Json

A divergence as the host reads it: {kind, at, clause, reason}.

cfamily.Dialect.notesJson

def Dialect.notesJson {L : Constructs} (d : Dialect L) (s : Option (State L)) : String

The divergences noted so far at a stop, as JSON.