state

cfamily.Stopped

record Stopped (L : Constructs)

Why a run stopped, and where: the node, and for a note the calls the run was in (the innermost call’s node first), so a problem in code a dialect generated is reported where the program called it; and the implementation’s choices the stop depends on (a block the library released only because of one).

cfamily.Stopped.of

def Stopped.of {L : Constructs} (n : NodeId) (w : Stopping L) : Stopped L

A stop or a note at a node for a reason.

cfamily.Stopped.at

def Stopped.at {L : Constructs} (n : NodeId) (b : Behavior) : Stopped L

A stop at a node for a behavior the standard leaves open.

cfamily.Scope

def Scope : Type

A scope: each declaration in it and its block.

cfamily.Stream

record Stream

A file the program opened: its name, whether it is read (else written, at the end), how many bytes have been read, whether reading reached the end, and whether it is still open.

cfamily.Chosen

record Chosen

A block whose fate a library left to an implementation’s choice: released (none), or kept and renumbered (its new number), and the choice. A pointer to the old number still reaches the object when it was kept, assuming the choice.

cfamily.Held

record Held

An array qsort or bsearch is sorting or searching, which the comparator is not to alter (C11 7.22.5p3): the block, the path to the array, and the elements from low up to high; for a pointer to a whole object (not an element), the object itself (range none).

cfamily.Orders

record Orders

Where comparing the two orders of indeterminately sequenced calls stands (cfamily.orders): whether the run is the other order’s trial (the points where the order of calls matters run in the first order there, not compared again), the points whose comparison is under way, the innermost first, each with the calls the run was in (one met again inside its own comparison, as a recursive call meets it, runs in the first order; a run that ends inside one ended before the comparison), and the budget left for comparing (the trials’ moves and the parts of the states compared).

cfamily.Orders.defaultBudget

def Orders.defaultBudget : Nat

The budget a run starts with when its fuel does not set one (the debugger’s runs).

cfamily.Orders.within

def Orders.within (budget : Nat) : Orders

Nothing compared yet, with a budget.

cfamily.State

record State (L : Constructs)

What a run changes: the memory, the scopes, the console, the divergences noted, the calls it is in (their nodes, the innermost first), where strtok goes on from (C11 7.24.5.8p3; none before its first call), the files (names to bytes; none at the start) and the streams the program opened (stream 3 on; 0 to 2 are stdin, stdout and stderr), the blocks left to an implementation’s choice, the arrays being sorted or searched (the innermost first), the words of glibc’s random number generator (the 34 most recent; none before the first rand or srand), where comparing the orders of calls stands, and the dialect’s part.

cfamily.State.start

def State.start {L : Constructs} (input : String) (extension : L.state) : State L

The state before a run: no blocks, one (the global) scope, the input on the console.

cfamily.State.findIn

def State.findIn (scope : Scope) (x : DeclId) : Option Nat

The block of a declaration in a scope.

cfamily.State.findAmong

def State.findAmong (scopes : List Scope) (x : DeclId) : Option Nat

The block of a declaration, innermost scope first.

cfamily.State.find

def State.find {L : Constructs} (s : State L) (x : DeclId) : Option Nat

The block a declaration names now.

cfamily.State.withMemory

def State.withMemory {L : Constructs} (s : State L) (m : Memory L) : State L

The memory replaced.

cfamily.State.withConsole

def State.withConsole {L : Constructs} (s : State L) (c : Console) : State L

The console replaced.

cfamily.State.withExtension

def State.withExtension {L : Constructs} (s : State L) (e : L.state) : State L

The dialect’s state replaced.

cfamily.Stopped.repeats

def Stopped.repeats {L : Constructs} (kept : List (Stopped L)) (w : Stopped L) : Bool

Whether a note says nothing a note already kept does: the same choice assumed (the verdict lists each choice once), or a divergence at the same node (the first is the one reported).

cfamily.State.addNote

def State.addNote {L : Constructs} (s : State L) (w : Stopped L) : State L

A note added (the first is the one reported), unless it repeats one kept: a loop that makes the same choice each time would otherwise keep a note for each, and adding at the end of a list that long is quadratic.

cfamily.State.enterScope

def State.enterScope {L : Constructs} (s : State L) : State L

A new innermost scope.

cfamily.State.releaseAll

def State.releaseAll {L : Constructs} (m : Memory L) (scope : Scope) : Memory L

Every block of a scope released.

cfamily.State.leaveScope

def State.leaveScope {L : Constructs} (s : State L) : State L

Leaving the innermost scope: its objects’ lifetimes end (C11 6.2.4p6).

cfamily.State.isolate

def State.isolate {L : Constructs} (s : State L) (x : DeclId) (b : Nat) : State L

An object moved out of the innermost scope into a scope of its own (its cleanup runs there: it can be named, and the scope it left does not find it again).

cfamily.State.bind

def State.bind (scopes : List Scope) (x : DeclId) (b : Nat) : List Scope

The declaration added to the innermost scope.

cfamily.State.declare

def State.declare {L : Constructs} (s : State L) (x : DeclId) (t : Ty L) (o : Object) (how : Allocation L) : State L

A new block for a declaration in the innermost scope.

cfamily.State.allocate

def State.allocate {L : Constructs} (s : State L) (t : Ty L) (o : Object) (how : Allocation L) : State L * Nat

A new block no declaration names (malloc), and its number.

cfamily.State.unbindIn

def State.unbindIn (scope : Scope) (x : DeclId) : Scope

The declaration removed from the innermost scope, its block kept (an object handed to the caller).

cfamily.State.unbind

def State.unbind {L : Constructs} (s : State L) (x : DeclId) : State L

The declaration no longer in the innermost scope.

cfamily.State.changeBlock

def State.changeBlock {L : Constructs} (s : State L) (x : DeclId) (f : Block L -> Block L) : State L

The declaration’s block changed, if it names one that is alive.

cfamily.State.assign

def State.assign {L : Constructs} (s : State L) (x : DeclId) (o : Object) : State L

The declaration’s object replaced.

cfamily.State.reallocate

def State.reallocate {L : Constructs} (s : State L) (x : DeclId) (how : Allocation L) : State L

The declaration’s allocation replaced (a slot is constructed, an object handed over).

cfamily.Object.zeroValue

def Object.zeroValue {L : Constructs} (t : Ty L) : Option Value

The zero of a scalar type: 0, the null pointer, positive zero.

cfamily.Making

record Making (L : Constructs)

How new objects are made: the dialect’s objects of its own types, and the place of a whole union kept as bits (none keeps it as a tree of members, cfamily.representation).

cfamily.Object.freshUnion

def Object.freshUnion {L : Constructs} (m : Making L) (zero : Bool) (t : Ty L) (xs : List Object) : Object

A new union: kept as bits when its type has a shape (zero: every bit 0 and the first member active), else a tree of members.

cfamily.Object.initializedUnion

def Object.initializedUnion {L : Constructs} (m : Making L) (t : Ty L) (k : Nat) (xs : List Object) : Object

A union initialized with its members’ objects, the k-th active: kept as bits (the member’s own, the rest indeterminate) when its type has a shape.

cfamily.Ty.isCharacter

def Ty.isCharacter {L : Constructs} (t : Ty L) : Bool

Whether a type is a character type (its objects are bytes).

cfamily.Ty.atPath

def Ty.atPath {L : Constructs} (t : Ty L) (path : List Nat) : Ty L

The type of the object at a path in an object of a type.

cfamily.Ty.elementOf

def Ty.elementOf {L : Constructs} (t : Ty L) : Ty L

The element type of an array type (a type that is not one is its own element).

cfamily.Pointer.bytesOf

def Pointer.bytesOf {L : Constructs} (m : Making L) (memory : Memory L) (element : Ty L) (p : Pointer) : Option Pointer

A pointer to elements of a type as a pointer to the bytes of the object it ranges over (C11 6.3.2.3p7): the object at its path (its first byte for a whole object, the element’s for one into an array), if the type has the C layout.

cfamily.Pointer.fromBytes

def Pointer.fromBytes {L : Constructs} (m : Making L) (element : Ty L) (p : Pointer) : Option Pointer

A pointer to bytes as a pointer to an object of a type at its first byte (the pointer the bytes came from, C11 6.3.2.3p7): the object at its path when it is of the type, an element of the array there; none when the byte is not where one begins.

cfamily.Pointer.asBytes

def Pointer.asBytes {L : Constructs} (m : Making L) (memory : Memory L) (p : Pointer) : Option Pointer

A pointer into a block as a pointer to the bytes of the object it ranges over, when its elements are not of a character type (their bytes are themselves) and have the C layout.