running

cfamily.ReasonKind

data ReasonKind

What a reason means for the verdict: undefined (reject), unspecified (unknown), or a termination the dialect defines (accept, C++’s std::terminate).

cfamily.ReasonDescription

record ReasonDescription

How a reason is reported: its code, clause, title and kind.

cfamily.ReasonDescription.undefined

def ReasonDescription.undefined (code : String) (clause : String) (title : String) : ReasonDescription

An undefined behavior’s description.

cfamily.OrderDifference.title

def OrderDifference.title (d : OrderDifference) : String

The words for how the two orders of calls differed, as d says.

cfamily.UncomparedReason.title

def UncomparedReason.title (r : UncomparedReason) : String

The words for why the two orders of calls were not compared, as r says.

cfamily.UncomparedReason.params

def UncomparedReason.params (r : UncomparedReason) : List (String * ParamValue)

Why the two orders of calls were not compared (r), as a problem’s params: budget or access.

cfamily.OrderDifference.params

def OrderDifference.params (d : OrderDifference) : List (String * ParamValue)

The details of how the two orders of calls differed (d), as a problem’s params: which part (output, state or end), and for the output, what each order wrote (output in the order run, otherOutput in the other).

cfamily.Behavior.describe

def Behavior.describe (rules : Rules) (b : Behavior) : ReasonDescription

The description of a behavior the standard leaves open; converting an out-of-range floating value is as the rules say (C’s unspecified value, C++’s undefined behavior).

cfamily.Dialect

record Dialect (L : Constructs)

A dialect: how it checks, evaluates and runs what the core does not know, how it makes new objects of its own types, how its reasons are reported, and its part of the state at the start.

cfamily.Dialect.check

def Dialect.check {L : Constructs} (d : Dialect L) : CheckDialect L

The checking dialect of expressions.

cfamily.Dialect.runDialect

def Dialect.runDialect {L : Constructs} (d : Dialect L) (c : CheckedProgram L) : RunDialect L

What running a checked program needs.

cfamily.Dialect.rules

def Dialect.rules {L : Constructs} (d : Dialect L) : Rules

The dialect’s rules.

cfamily.Dialect.describeStop

def Dialect.describeStop {L : Constructs} (d : Dialect L) (w : Stopped L) : ReasonDescription

How a stop is reported.

cfamily.Problem

record Problem

A problem in a verdict: its details (params) when it is structured, from which the reason is made; a problem not structured yet has none (a host sees which).

cfamily.Problem.plain

def Problem.plain (kind : String) (category : String) (at : NodeId) (clause : String) (reason : String) : Problem

A problem not structured yet, of kind and category, at the node at (with the standard’s clause): the reason in words only.

cfamily.Problem.categoryOf

def Problem.categoryOf (k : ReasonKind) : String

A problem’s category from k, the kind of its reason (the verdict JSON’s category, by which a host shows it): undefined behavior is the program’s error, an unspecified or implementation-defined result the run cannot settle is indeterminate, a defined way to end (abort, an uncaught exception) is a termination.

cfamily.Problem.optionalParam

def Problem.optionalParam (name : String) (value : Option String) : List (String * ParamValue)

The param name with the text value when there is one (none leaves an optional param out).

cfamily.Behavior.boundsParams

def Behavior.boundsParams (index : Option Int) (size : Option Nat) : List (String * ParamValue)

The details of a pointer out of bounds, as a problem’s params: the index it would have (an offset from the array’s start, in decimal) and the array’s size (its number of elements), each when known.

cfamily.Behavior.overflowParams

def Behavior.overflowParams (boolean : String) (type : IntegerType) (operator : String) (operands : List Int) : List (String * ParamValue)

The details of a signed overflow, as a problem’s params: the type (its name; boolean names the boolean type), the operator, and the operands, left and, for a binary operation, right (each in decimal).

cfamily.Behavior.params

def Behavior.params (rules : Rules) (b : Behavior) : Option (List (String * ParamValue))

The details of b, a behavior the standard leaves open, when its problem is structured: how two orders of calls differed or why they were not compared, where a pointer went out of bounds, the operator that divided by zero (/ or %), and the operation that overflowed (its type named as the rules’ dialect names types).

cfamily.Stopped.params

def Stopped.params {L : Constructs} (rules : Rules) (w : Stopped L) : Option (List (String * ParamValue))

The details of w, a stop or a note, when its problem is structured (Behavior.params, by the rules).

cfamily.Dialect.problem

def Dialect.problem {L : Constructs} (d : Dialect L) (w : Stopped L) : Problem

The problem a stop or a note is (structured when it has details).

cfamily.RunResult

record RunResult

A verdict: accept, reject, unknown or invalid; the exit code if the program exited; the output; the problems; the implementation’s choices it assumes (made as libc++ makes them, each named once); the steps its run took (in fuel’s unit: the fuel when it ran out, 0 when the program did not run).

cfamily.RunResult.of

def RunResult.of (verdict : String) (problems : List Problem) : RunResult

A verdict with no exit code and no output (and no steps yet).

cfamily.RunResult.exited

def RunResult.exited (verdict : String) (problems : List Problem) (code : Int) (out : String) : RunResult

A program that exited: the verdict, the problems, the exit code and the output (and no steps yet).

cfamily.RunResult.afterSteps

def RunResult.afterSteps (fuel : Nat) (left : Nat) (r : RunResult) : RunResult

The verdict r of a run given fuel steps that finished with left of them unused: it took the rest.

cfamily.Stopped.choice

def Stopped.choice {L : Constructs} (w : Stopped L) : Option String

The choice a note assumes, if it is one (else the note is a divergence from the standard).

cfamily.Stopped.choices

def Stopped.choices {L : Constructs} (w : Stopped L) : List String

The choice a note assumes, as a list (empty for a divergence).

cfamily.Stopped.diverges

def Stopped.diverges {L : Constructs} (w : Stopped L) : Bool

Whether a note is a divergence from the standard (not an assumed choice).

cfamily.RunResult.once

def RunResult.once (seen : List String) (xs : List String) : List String

Names with each kept once, the first time it comes.

cfamily.RunResult.assuming

def RunResult.assuming {L : Constructs} (notes : List (Stopped L)) (more : List String) (r : RunResult) : RunResult

A verdict with the choices its run’s notes (and its stop) assume.

cfamily.RunResult.outOfStepsWith

def RunResult.outOfStepsWith (params : List (String * ParamValue)) : RunResult

Running out of steps, with the problem’s params (a structured problem: the reason is the same with or without).

cfamily.RunResult.outOfSteps

def RunResult.outOfSteps : RunResult

Running out of steps, or of the evaluation’s depth (a structured problem; no details).

cfamily.RunResult.pastStepLimit

def RunResult.pastStepLimit (steps : Nat) : RunResult

Running out of steps after the run’s limit, steps of them (the problem’s steps param, in decimal).

cfamily.RunResult.notChecked

def RunResult.notChecked (n : NodeId) (why : Refusal) : RunResult

A program that did not check at the node n, refused for why: an empty slot is unknown, anything else rejected (a structured refusal with its kind and details).

cfamily.RunResult.notProvided

def RunResult.notProvided (n : NodeId) (construct : String) : RunResult

A program using a construct the model does not provide: unknown, the construct named (the program may be valid).

cfamily.Stopped.placed

def Stopped.placed {L : Constructs} (source : NodeId -> Bool) (callers : List NodeId) (w : Stopped L) : Stopped L

A stop or a note placed in the program: at its node if the program has it, else at the innermost call the program made (a problem in code a dialect generated, such as a library’s, is the call’s).

cfamily.Program.mentions

def Program.mentions (n : NodeId) (p : Program) : Bool

Whether a node is one of the program’s.

cfamily.NodeId.isLibrary

def NodeId.isLibrary (n : NodeId) : Bool

Whether a node is a library’s (lib: and its header’s place: code a dialect put in the program for it).

cfamily.Program.wrote

def Program.wrote (n : NodeId) (p : Program) : Bool

Whether a node is one the program itself wrote (not a library’s put in it).

cfamily.Program.written

def Program.written (p : Program) : List NodeId

The nodes the program itself wrote (Program.wrote), all of them: what the debugger stops at.

cfamily.Program.madeFrom

def Program.madeFrom (p : Program) (n : NodeId) (parts : List String) : NodeId

The written node a dialect’s pass made n from, given n’s parts between colons, last first: the longest part before a colon the program wrote (c8:object, nw:length, C:made:copy), else n.

cfamily.Program.placedNode

def Program.placedNode (p : Program) (n : NodeId) : NodeId

The node a checking problem is reported at: its own if the program wrote it, else the one it was made from by a dialect’s pass (Program.madeFrom), else as it is.

cfamily.Dialect.headerChoices

def Dialect.headerChoices {L : Constructs} (d : Dialect L) (program : Program) : List String

The choices a program’s headers assume (a library’s non-standard header, cfamily.rules).

cfamily.Item.useLongDouble

def Item.useLongDouble (items : List Item) : Bool

Whether the items use long double: write the type (a declaration, a cast, sizeof, a template argument…) or a constant with the suffix l or L.

cfamily.Dialect.platformChoices

def Dialect.platformChoices {L : Constructs} (d : Dialect L) (program : Program) : List String

The choices of the platform a program assumes: long double’s format (Target.longDoubleChoice) when the program uses long double, whose size, alignment and precision the platform chooses (C11 6.2.5p10); a verdict that depends on them is the target’s.

cfamily.Dialect.programChoices

def Dialect.programChoices {L : Constructs} (d : Dialect L) (program : Program) : List String

The choices a program assumes before its run’s: its headers’ (Dialect.headerChoices), then its platform’s (Dialect.platformChoices).

cfamily.RunResult.assumingFirst

def RunResult.assumingFirst (choices : List String) (r : RunResult) : RunResult

A verdict with more choices assumed before its own (each once).

cfamily.State.settledNotes

def State.settledNotes {L : Constructs} (notes : List (Stopped L)) (comparing : List (NodeId * List NodeId)) : List (Stopped L)

The notes of a state with the comparisons of orders still under way (comparing: the run ended inside the first order) noted as divergences, the outermost first: the other order may end otherwise.

cfamily.State.settled

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

A run’s last state with the comparisons of orders still under way noted (State.settledNotes).

cfamily.Dialect.resultOf

def Dialect.resultOf {L : Constructs} (d : Dialect L) (source : NodeId -> Bool) (o : Outcome L) : RunResult

The verdict of a run’s outcome: an exit is accept, or unknown after a divergence (the first note); a stop is as its reason’s kind says. The problems are placed in the program (source says which nodes are its).

cfamily.Configuration.budgeted

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

The run’s start x with the budget for comparing the orders of calls: half its fuel (the comparisons’ moves are moves of the run; past the budget the orders are noted as not compared, and the run keeps the other half).

cfamily.RunDialect.runLeft

def RunDialect.runLeft {L : Constructs} (d : RunDialect L) (fuel : Nat) (x : Configuration L) : Configuration L * Nat

At most fuel moves of the dialect d from x, until the run finishes: where it got, and the fuel left unused.

cfamily.RunDialect.runFor

def RunDialect.runFor {L : Constructs} (d : RunDialect L) (fuel : Nat) (x : Configuration L) : Configuration L

At most fuel moves of the dialect d from x, until the run finishes (RunDialect.runLeft without the fuel left).

cfamily.Dialect.startWith

def Dialect.startWith {L : Constructs} (d : Dialect L) (c : CheckedProgram L) (input : String) (given : List String) : Configuration L

The start of a checked program’s run on an input and the program’s arguments.

cfamily.Dialect.defaultArguments

def Dialect.defaultArguments : List String

The program’s arguments when none are given: its name only (argc is 1).

cfamily.Dialect.start

def Dialect.start {L : Constructs} (d : Dialect L) (c : CheckedProgram L) (input : String) : Configuration L

The start of a checked program’s run on an input, with the default arguments.

cfamily.Dialect.verdictWithArguments

def Dialect.verdictWithArguments {L : Constructs} (d : Dialect L) (fuel : Nat) (input : String) (given : List String) (program : Program) : RunResult

Checks the program in the dialect d and runs it on the input and the program’s arguments given for at most fuel steps; the verdict assumes the program’s choices (Dialect.programChoices) before its run’s.

cfamily.Dialect.verdictCheckedWithArguments

def Dialect.verdictCheckedWithArguments {L : Constructs} (d : Dialect L) (fuel : Nat) (input : String) (given : List String) (program : Program) : RunResult

As Dialect.verdictWithArguments, without the choices the program assumes (its headers’, its platform’s).

cfamily.Outcome.extension

def Outcome.extension {L : Constructs} (o : Outcome L) : Option L.state

The dialect’s state at the end of a run (none when it did not finish or the program was not checked).

cfamily.Dialect.verdictAndState

def Dialect.verdictAndState {L : Constructs} (d : Dialect L) (fuel : Nat) (input : String) (program : Program) : RunResult * Option L.state

Checks a program and runs it on an input for at most fuel steps, with the default arguments: the verdict, and the dialect’s state at the end (what a host shows of the program’s environment).

cfamily.Dialect.verdictAndStateWritten

def Dialect.verdictAndStateWritten {L : Constructs} (d : Dialect L) (fuel : Nat) (input : String) (program : Program) (written : Program) : RunResult * Option L.state

As Dialect.verdictAndState (the dialect d, the program run on the input for at most fuel steps), the problems placed in what the program wrote (written: a dialect may run more, such as a board’s items and the sketch rewritten for them); the verdict assumes the program’s choices (Dialect.programChoices).

cfamily.Dialect.verdictAndStateChecked

def Dialect.verdictAndStateChecked {L : Constructs} (d : Dialect L) (fuel : Nat) (input : String) (program : Program) (written : Program) : RunResult * Option L.state

As Dialect.verdictAndStateWritten, without the choices the program assumes (its headers’, its platform’s).

cfamily.Dialect.verdictOf

def Dialect.verdictOf {L : Constructs} (d : Dialect L) (fuel : Nat) (input : String) (program : Program) : RunResult

Checks a program and runs it on an input for at most fuel steps, with the default arguments.

cfamily.Problem.json

def Problem.json (p : Problem) : Json

A problem as JSON.

cfamily.RunResult.choiceJson

def RunResult.choiceJson (c : String) : Json

An assumed choice as JSON: the implementation it is made as (the part before a colon, else libc++), and its name.

cfamily.RunResult.fields

def RunResult.fields (r : RunResult) : List (String * Json)

A verdict’s JSON fields: verdict, basis, exit, out, problems, and assumes, the implementation’s choices it assumes, always there so a host can check them against itself before running (a dialect with more to say, a board’s hardware, adds its own after them).

cfamily.RunResult.json

def RunResult.json (r : RunResult) : String

A verdict as JSON: its fields (RunResult.fields).

cfamily.RunResult.withSteps

def RunResult.withSteps (r : RunResult) (fields : List (String * Json)) : List (String * Json)

The fields of a verdict’s JSON (the verdict’s own, and any a dialect adds after them) with the steps the run of r took after them all, the last field: what a host bounds a run by, the same on every host.

cfamily.RunResult.reportFields

def RunResult.reportFields (r : RunResult) : List (String * Json)

A verdict’s report’s fields: the verdict r’s (RunResult.fields), then the steps its run took (RunResult.withSteps).

cfamily.RunResult.reportJson

def RunResult.reportJson (r : RunResult) : String

A verdict’s report as JSON: the verdict r’s JSON with the steps its run took as the last field (RunResult.reportFields); without that field it is the verdict’s JSON (RunResult.json).