statements

cfamily.StatementContext

record StatementContext (L : Constructs)

Where a statement is: the tables, the function’s result type (none is void), whether break (in a loop or switch) and continue (in a loop) are allowed, the labels in reach with the block each belongs to, and every label of the function (a goto to one out of reach is valid C the model does not run).

cfamily.StatementContext.loop

def StatementContext.loop {L : Constructs} (c : StatementContext L) : StatementContext L

The context inside a loop: break and continue are allowed.

cfamily.StatementContext.switch

def StatementContext.switch {L : Constructs} (c : StatementContext L) : StatementContext L

The context inside a switch: break is allowed.

cfamily.LiftedInit

record LiftedInit (L : Constructs)

An initializer checked: the statements it needs first, the typed initializer, its accesses.

cfamily.StatementChecker

record StatementChecker (L : Constructs)

The core’s statement checking functions, for a dialect checking its own statements and initializers (an initializer of a known type, as a declaration checks it).

cfamily.StatementExtension

record StatementExtension (L : Constructs)

How a dialect checks what the core does not know about statements. Each gives none to leave it to the core.

• statement: its own statements;
• declaration: declaring an object of its types (constructors, std::vector, a device on a board);
• expressionStatement: an expression statement it handles (std::swap, a member call whose result is dropped);
• condition: a condition of its types (a class’s operator bool);
• endOfFullExpression: what ends with a full expression (C++’s temporaries; the statement itself otherwise);
• returnValue: returning a value of its types (a return slot, a move);
• declared: the variable one of its statements declares, with its type.

cfamily.StatementExtension.empty

def StatementExtension.empty {L : Constructs} : StatementExtension L

The statement extension of a dialect without statements of its own.

cfamily.StatementDialect

record StatementDialect (L : Constructs)

What checking statements needs of a dialect: what checking expressions needs, and its statement extension.

cfamily.LiftedInit.of

def LiftedInit.of {L : Constructs} (before : List (TypedStmt L)) (init : TypedInit L) (writes : List (MemoryAccess L)) (reads : List (MemoryAccess L)) : LiftedInit L

An initializer with its statements, writes and reads.

cfamily.TypedStmt.after

def TypedStmt.after {L : Constructs} (n : NodeId) (before : List (TypedStmt L)) (s : TypedStmt L) : TypedStmt L

The statements before a statement, and the statement: one sequence (one stop), or the statement alone.

cfamily.TypedStmt.ofAll

def TypedStmt.ofAll {L : Constructs} (n : NodeId) (ss : List (TypedStmt L)) : TypedStmt L

Statements in a statement’s place: one is itself, else a sequence.

cfamily.TypedStmt.alone

def TypedStmt.alone {L : Constructs} (s : TypedStmt L) : TypedStmt L

A statement in a place of exactly one (a branch, a loop body): a sequence is wrapped in a block without a node, so its temporaries end each time it is left.

cfamily.Stmt.isFullExpression

def Stmt.isFullExpression (s : Stmt) : Bool

Whether a statement is a full expression (its temporaries end after it).

cfamily.Init.stringLength

def Init.stringLength (str : String) : Nat

The length of the array a string literal is: its characters and the null.

cfamily.StatementDialect.declaredType

def StatementDialect.declaredType {L : Constructs} (sd : StatementDialect L) (g : Globals L) (n : NodeId) (t : TypeSyntax) (i : Option Init) : CheckResult L (Ty L)

The type of a declaration: an array of unknown length takes it from the initializer (a list’s length, a string’s with the null), C11 6.7.9p22.

cfamily.StatementDialect.declaredIn

def StatementDialect.declaredIn {L : Constructs} (sd : StatementDialect L) (g : Globals L) (env : Env L) (s : Stmt) : Env L

The scope env after the statement s: what it declares added (a declaration, a variable length array, a label’s statement, the dialect’s), its types resolved by the dialect sd with the globals g.

cfamily.Stmt.variableLength

def Stmt.variableLength (s : Stmt) : Stmt

A block’s declaration of an array whose length is an expression that is not a constant (cfamily.lengths made the constant ones tArr), without an initializer: a variable length array (C11 6.7.6.2p4), as sDeclV.

cfamily.StatementDialect.concrete

def StatementDialect.concrete {L : Constructs} (sd : StatementDialect L) (c : StatementContext L) (env : Env L) (s : Stmt) : CheckResult L Stmt

The statement s as the dialect sd makes it concrete before checking it in the context c and the scope env (itself when the dialect does nothing; a variable length array written as a declaration is sDeclV first, Stmt.variableLength).

cfamily.Stmt.concreteOr

def Stmt.concreteOr {L : Constructs} (made : CheckResult L Stmt) (s : Stmt) : Stmt

The concrete statement when made gives one, else the statement s as written.

cfamily.StatementDialect.declaredInAll

def StatementDialect.declaredInAll {L : Constructs} (sd : StatementDialect L) (g : Globals L) (env : Env L) (ss : List Stmt) : Env L

The scope after statements, in order.

cfamily.StatementContext.withLabels

def StatementContext.withLabels {L : Constructs} (c : StatementContext L) (n : NodeId) (ss : List Stmt) : StatementContext L

The labels that are direct statements of a block, each with the block (goto may jump to them, C11 6.8.6.1).

cfamily.Init.character

def Init.character {L : Constructs} (m : NodeId) (element : IntegerType) (ch : Char) : TypedInit L

A character of a string initializing an array element.

cfamily.StatementDialect.stringInit

def StatementDialect.stringInit {L : Constructs} (sd : StatementDialect L) (m : NodeId) (element : IntegerType) (k : Nat) (str : String) : CheckResult L (LiftedInit L)

A string initializing a char array: each character, the null if there is room; too long is rejected, and by the rules C++ needs room for the null (C11 6.7.9p14, C++ [dcl.init.string]p2).

cfamily.StatementDialect.expressionInit

def StatementDialect.expressionInit {L : Constructs} (sd : StatementDialect L) (g : Globals L) (env : Env L) (n : NodeId) (t : Ty L) (e : Expr) : CheckResult L (LiftedInit L)

An expression initializing an object of type t: checked against t, converted as if by assignment.

cfamily.Narrowing

data Narrowing

Whether a braced list’s element narrows ([dcl.init.list]p7): not; does (the reason); or may, where it narrows unless it is a constant expression this does not evaluate (a const variable’s value).

cfamily.Expr.smallFloatLiteral

def Expr.smallFloatLiteral (e : Expr) : Bool

Whether the floating literal e, possibly negated, is within a float’s range: written without an exponent and with at most 30 digits before the point (a float holds up to about 3.4e38).

cfamily.Expr.readsConstant

def Expr.readsConstant {L : Constructs} (env : Env L) (e : Expr) : Bool

Whether e reads a variable that may be a constant expression’s: a const one, or one not among the locals env.

cfamily.Narrowing.of

def Narrowing.of {L : Constructs} (g : Globals L) (env : Env L) (e : Expr) (source : Ty L) (target : Ty L) : Narrowing

Whether the element e of a braced list, whose value has the type source (constants g’s), narrows when converted to the type target (C++ [dcl.init.list]p7): a floating type to an integer type (7.1); a floating type to a narrower one (7.2), unless a literal within range; an integer type to a floating type (7.3) or to one that does not hold all its values (7.4), unless a constant that fits. The types are the expression’s and the object’s, so a cast written in e (100ULL, (char)x) is the expression’s own type, not a narrowing. A conversion that narrows unless e is a constant expression is only maybe so when e reads a variable that may be one (in the scope env).

cfamily.StatementDialect.listedInit

def StatementDialect.listedInit {L : Constructs} (sd : StatementDialect L) (g : Globals L) (env : Env L) (n : NodeId) (t : Ty L) (e : Expr) : CheckResult L (LiftedInit L)

The element e of a braced list initializing an object of type t, declared at n (by sd, with g and the scope env): as an expression’s initializer (checked against t, converted as by assignment), and not narrowed where the dialect forbids it (Narrowing.of, from the type of e’s value).

cfamily.Init.repeated

def Init.repeated {L : Constructs} (u : Ty L) (xs : List Init) : List (Ty L)

The element type once per initializer.

cfamily.FieldTy.type

def FieldTy.type {L : Constructs} (f : FieldTy L) : Ty L

The type of a member.

cfamily.Init.memberTypes

def Init.memberTypes {L : Constructs} (fs : List (FieldTy L)) (xs : List Init) : List (Ty L)

The types of the first members, one per initializer.

cfamily.LiftedInit.both

def LiftedInit.both {L : Constructs} (n : NodeId) (a : LiftedInit L) (rest : LiftedInit L) : LiftedInit L

Two initializers unsequenced (the elements of a list, C11 6.7.9p23).

cfamily.CheckResult.isChecked

def CheckResult.isChecked {L : Constructs} {A : Type} (r : CheckResult L A) : Bool

Whether a check succeeded.

cfamily.Expr.constantValue

def Expr.constantValue (constants : List (DeclId * Int)) (e : Expr) : Option Int

The value of an integer constant expression (C11 6.6): literals, character constants, enumeration constants, and their negation, sum, difference and product.

cfamily.Ty.isAggregate

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

Whether a type is an aggregate whose braces an initializer list may elide (an array, a struct or a union).

cfamily.Init.isList

def Init.isList (x : Init) : Bool

Whether an initializer is a brace-enclosed list.

cfamily.Init.isDesignated

def Init.isDesignated (x : Init) : Bool

Whether an initializer has a designator (.x = 1, [2] = 5).

cfamily.Init.isStringFor

def Init.isStringFor {L : Constructs} (t : Ty L) (x : Init) : Bool

Whether an initializer is a string literal for a character array (it initializes the array by itself).

cfamily.Ty.slots

def Ty.slots {L : Constructs} (t : Ty L) : List (Ty L)

The types of the subobjects an initializer list fills in order: an array’s elements, a struct’s members (an unnamed bit-field takes none; an anonymous struct or union is one, C11 6.7.2.1p13), a union’s first member.

cfamily.Init.regroup

def Init.regroup {L : Constructs} (sd : StatementDialect L) (g : Globals L) (env : Env L) (n : NodeId) (slots : List (Ty L)) (xs : List Init) : CheckResult L (List Init)

An initializer list with the braces it elides put back (C11 6.7.9p20, [dcl.init.aggr]p15), for subobjects of the slots’ types in order: an initializer that is a list, a string for a character array, or an expression that initializes the subobject whole (a struct of its type) stays as it is; otherwise the subobject takes as many initializers from the list as it needs (Ty.elidedCount), as a list. Initializers past the slots stay as they are (too many). A list among the ones taken (braces inside an elided subobject) is not modeled.

cfamily.Designator.memberPlace

def Designator.memberPlace {L : Constructs} (name : String) (k : Nat) (fs : List (FieldTy L)) : Option (Nat * Bool)

The place among a struct’s slots of the member of a name, and whether it is inside the anonymous struct or union at that place (C11 6.7.2.1p13: its members are the struct’s; the designator then goes on into it).

cfamily.Designator.place

def Designator.place {L : Constructs} (g : Globals L) (t : Ty L) (d : Designator) : Option (Nat * Bool)

The slot a designator names in an aggregate of a type (C11 6.7.9p6-7): a struct’s member, or an array’s element by an index within its length, and whether the designator goes on into the slot (a member of an anonymous struct or union); none when it names none.

cfamily.Init.cellsWith

def Init.cellsWith (cells : List (Option Init)) (k : Nat) (m : NodeId) (rest : List Designator) (value : Init) : List (Option Init)

The cells of an aggregate’s slots with one set: a whole initializer replaces the cell; one for a part of it (a longer designator path) is added to the cell’s list.

cfamily.Init.Filling

def Init.Filling : Type

The slots filled so far while designators are put in place, and the next slot.

cfamily.Init.positioned

def Init.positioned {L : Constructs} (sd : StatementDialect L) (g : Globals L) (env : Env L) (n : NodeId) (t : Ty L) (xs : List Init) : CheckResult L (List Init)

An initializer list with designators put in the positions of a type’s slots (C11 6.7.9p17-19): a designator moves to its slot, an initializer without one goes to the slot after the last; a slot set twice keeps the later; a slot left empty is zero (an empty list for an aggregate). An initializer without a designator that falls on an aggregate slot without its own braces (braces elided after a designator) is not modeled.

cfamily.Init.listLength

def Init.listLength (constants : List (DeclId * Int)) (xs : List Init) : Nat

The length of an array an initializer list gives (C11 6.7.9p22): one past the last element it initializes, with designators.

cfamily.Init.bracingDepth

def Init.bracingDepth : Nat

The levels of nesting Init.braced goes down at most (a type nests its aggregates fewer times than that).

cfamily.StatementDialect.condition

def StatementDialect.condition {L : Constructs} (sd : StatementDialect L) (g : Globals L) (n : NodeId) (l : Lifted L) : CheckResult L (Lifted L)

A condition: a scalar, the dialect’s conversion for its types first (C11 6.8.4.1p1, 6.8.5p2).

cfamily.Signature.droppedInto

def Signature.droppedInto {L : Constructs} (m : NodeId) (sg : Signature L) : Option (DeclId * Ty L)

The temporary a dropped result still is: a structure’s or a class’s (whose end the dialect may run something for, a destructor, [class.temporary]p4), none for a scalar or no result.

cfamily.StatementDialect.callStatement

def StatementDialect.callStatement {L : Constructs} (sd : StatementDialect L) (c : StatementContext L) (env : Env L) (n : NodeId) (m : NodeId) (f : String) (args : List Expr) : CheckResult L (TypedStmt L)

The call of a function whose result is dropped (a statement): the arguments converted; a temporary only for a result of a structure or a class (it ends with the full expression).

cfamily.StatementDialect.releaseNull

def StatementDialect.releaseNull {L : Constructs} (m : NodeId) (p : TypedExpr L) : TypedStmt L

free of a null pointer constant (it does nothing, C11 7.22.3.3p2).

cfamily.StatementDialect.freeStatement

def StatementDialect.freeStatement {L : Constructs} (sd : StatementDialect L) (g : Globals L) (env : Env L) (n : NodeId) (m : NodeId) (args : List Expr) : CheckResult L (TypedStmt L)

free(p): p is a pointer (or a null pointer constant).

cfamily.StatementDialect.exitStatement

def StatementDialect.exitStatement {L : Constructs} (sd : StatementDialect L) (g : Globals L) (env : Env L) (n : NodeId) (m : NodeId) (args : List Expr) : CheckResult L (TypedStmt L)

exit (C11 7.22.4.4): the run ends normally, the status its exit code; nothing after it runs. A status known when checking (a constant, EXIT_FAILURE) is supported; one computed while running is not yet.

cfamily.StatementDialect.abortStatement

def StatementDialect.abortStatement {L : Constructs} (m : NodeId) (args : List Expr) : CheckResult L (TypedStmt L)

abort (C11 7.22.4.1): the program ends abnormally, a termination the standard defines.

cfamily.StatementDialect.assertStatement

def StatementDialect.assertStatement {L : Constructs} (sd : StatementDialect L) (g : Globals L) (env : Env L) (n : NodeId) (m : NodeId) (args : List Expr) : CheckResult L (TypedStmt L)

assert (C11 7.2.1.1, a macro of <assert.h>): when the condition is false the program aborts. Without the header the name is undeclared.

cfamily.CheckDialect.evaluatedStatement

def CheckDialect.evaluatedStatement {L : Constructs} (d : CheckDialect L) (g : Globals L) (env : Env L) (n : NodeId) (e : Expr) : CheckResult L (TypedStmt L)

An expression statement’s expression evaluated and its value dropped.

cfamily.StatementDialect.expressionStatement

def StatementDialect.expressionStatement {L : Constructs} (sd : StatementDialect L) (c : StatementContext L) (env : Env L) (n : NodeId) (e : Expr) : CheckResult L (TypedStmt L)

An expression statement: the dialect’s first; calls drop their results (void functions included, by name or through a pointer, and a cast to void, C11 6.5.4p2); an assignment or an increment is its statements (postfix as prefix: the value is not used); else the value is evaluated for its undefined behavior.

cfamily.StatementDialect.returnStatement

def StatementDialect.returnStatement {L : Constructs} (sd : StatementDialect L) (c : StatementContext L) (env : Env L) (n : NodeId) (e : Option Expr) : CheckResult L (TypedStmt L)

return: with a value converted to the result type (the dialect’s for its types), without one in a void function.

cfamily.StatementDialect.declarationOf

def StatementDialect.declarationOf {L : Constructs} (sd : StatementDialect L) (c : StatementContext L) (env : Env L) (n : NodeId) (x : DeclId) (name : String) (t : TypeSyntax) (i : Option Init) : CheckResult L (TypedStmt L)

A declaration of a type that is not a variable length array (StatementDialect.declaration).

cfamily.CheckDialect.variableArray

def CheckDialect.variableArray {L : Constructs} (d : CheckDialect L) (c : StatementContext L) (env : Env L) (n : NodeId) (x : DeclId) (name : String) (t : TypeSyntax) (len : Expr) : CheckResult L (TypedStmt L)

A variable length array (by the rules): the element type complete, the length an integer (as long). As an implementation’s extension, the run notes that it assumes it.

cfamily.StatementDialect.declaration

def StatementDialect.declaration {L : Constructs} (sd : StatementDialect L) (c : StatementContext L) (env : Env L) (n : NodeId) (x : DeclId) (name : String) (t : TypeSyntax) (i : Option Init) : CheckResult L (TypedStmt L)

A declaration: the dialect’s for objects of its types; an incomplete type is rejected; with an initializer, its statements first.

cfamily.TypedStmt.target

def TypedStmt.target {L : Constructs} (target : Option (DeclId * Ty L)) : List DeclId

The variable a call’s result goes into, if any.

cfamily.TypedStmt.endingTemporaries

def TypedStmt.endingTemporaries {L : Constructs} (n : NodeId) (x : TypedStmt L) : TypedStmt L

A full expression’s statement followed by the end of its temporaries, the last created first (C11 6.2.4p8).

cfamily.Lifted.settled

def Lifted.settled {L : Constructs} (d : CheckDialect L) (n : NodeId) (l : Lifted L) : Lifted L

A condition whose statements create temporaries: its value kept in a temporary of its own, named by the condition’s node with :condition (the node alone may already name one of the temporaries: a call’s result of reference type is what it refers to at the call’s node, v[i] of a vector), then the temporaries end, before the branch is taken.

cfamily.Stmt.recovered

def Stmt.recovered {L : Constructs} (g : Globals L) (r : CheckResult L (TypedStmt L)) : CheckResult L (TypedStmt L)

In the type query’s collect mode, a statement that does not check is recorded and checking goes on; otherwise the error stands.

cfamily.StatementChecker.fuel

def StatementChecker.fuel : Nat

The fuel for checking one function body: deeper nesting of statements is rejected.

cfamily.Stmt.check

def Stmt.check {L : Constructs} (sd : StatementDialect L) (c : StatementContext L) (env : Env L) (s : Stmt) : CheckResult L (TypedStmt L)

Checks a statement in a context and scope.

cfamily.Stmt.checkAll

def Stmt.checkAll {L : Constructs} (sd : StatementDialect L) (c : StatementContext L) (env : Env L) (ss : List Stmt) : CheckResult L (List (TypedStmt L))

Checks the statements of a block in a context and scope.

cfamily.StatementChecker.of

def StatementChecker.of {L : Constructs} (sd : StatementDialect L) : StatementChecker L

The core’s statement checker, for a dialect.