program

cfamily.CheckedFunction

record CheckedFunction (L : Constructs)

A checked function: its node, name, parameters (with their types) and body.

cfamily.CheckedProgram

record CheckedProgram (L : Constructs)

A checked program: its functions, the statements that initialize the globals (in order, before main), and the tables checking built (running needs the types’ sizes), and the functions checked only if used (ProgramExtension.lazy) not checked yet, each with the globals before it.

cfamily.ProgramExtension

record ProgramExtension (L : Constructs)

How a dialect takes part in checking a program. Each has a default that leaves it to the core.

• entry: the function a run starts at (main in C and C++; a board’s core names its own: ESP32’s app_main);
• prepare: the dialect’s passes on the items before checking (none of the dialect’s items may be left that the core or the dialect’s other extensions do not check), given also the entry’s name and the types the type query puts in the program’s holes (they are used as much as the types the program writes: C++ brings in the library that declares them);
• tables: what the dialect adds to the tables, from the items;
• answer: the program’s items with what a request of checking needs added (none: the request cannot be met); the program is then prepared and checked again;
• parameterType: how a parameter of a type is passed (C++ passes a class with a nontrivial copy by reference);
• functionBody: a function’s checked body wrapped (C++: a noexcept function’s boundary);
• effectFunctions: functions whose bodies the effect summaries also need (function templates);
• instantiate: the definition of a function template’s instance by its name (f<int>), made from the template when a call deduces it and the program does not have it (checked as a deferred function, as Clang instantiates pending definitions at the end); none to ask for it instead (a request: the program prepared and checked again).

cfamily.ProgramDialect

record ProgramDialect (L : Constructs)

What checking a program needs of a dialect.

cfamily.ProgramDialect.check

def ProgramDialect.check {L : Constructs} (pd : ProgramDialect L) : CheckDialect L

The dialect’s checking of expressions.

cfamily.Item.structs

def Item.structs (union : Bool) (items : List Item) : List (String * List (String * TypeSyntax))

The structs (or unions) of the items with their members as written.

cfamily.StructDefinition.entry

def StructDefinition.entry (d : StructDefinition) : String * List (String * TypeSyntax)

A struct or union’s name and members as written.

cfamily.Field.entry

def Field.entry (f : Field) : String * TypeSyntax

A member’s name and type as written.

cfamily.Item.duplicateTag

def Item.duplicateTag (items : List Item) : Option (NodeId * String)

The first name defined twice among struct and union tags (they share one name space, C11 6.2.3).

cfamily.TypeSyntax.needsUndefined

def TypeSyntax.needsUndefined (defined : List String) (t : TypeSyntax) : Bool

Whether a member’s written type needs a struct or union not yet defined (not behind a pointer): a member’s type is complete (C11 6.7.2.1p3), and a struct is complete only after its closing brace (6.7.2.1p8).

cfamily.Item.incompleteMember

def Item.incompleteMember (defined : List String) (items : List Item) : Option NodeId

The first struct or union with a member of a type not yet complete there (itself, or one defined after it).

cfamily.StructDefinition.tag

def StructDefinition.tag (d : StructDefinition) : NodeId * String

A struct or union’s node and name.

cfamily.Program.firstRepeated

def Program.firstRepeated (seen : List String) (xs : List (NodeId * String)) : Option (NodeId * String)

The first name repeated in the list, with the node of its repetition.

cfamily.Program.enumerators

def Program.enumerators {L : Constructs} (s : ConstantScope) (fixed : Option IntegerType) (n : NodeId) (next : Int) (cs : List Enumerator) : CheckResult L (List (DeclId * Int))

The enumeration constants cs of an enum (at the node n), with the constants known in the scope s: without a value the previous plus one (next; the first is 0); a value is an integer constant expression (ConstantScope.value; one the model does not decide is unknown); each fits int (C11 6.7.2.2p2), or the fixed underlying type of a scoped enumeration (C++ [dcl.enum]p5: a value written is converted to it without narrowing, one counted must be representable).

cfamily.Program.outOfRange

def Program.outOfRange (u : IntegerType) (written : Bool) (v : Int) : String

Why the value v of an enumeration constant does not fit the fixed underlying type u (clang’s words; written: the source gives the value, else it is counted from the one before).

cfamily.Program.fixedType

def Program.fixedType (s : ConstantScope) (base : Option TypeSyntax) : Option IntegerType

The underlying type of a scoped enumeration with the written base, in the scope s: int without one (C++ [dcl.enum]p5), none when the base is not an integer type.

cfamily.Program.enumerator

def Program.enumerator {L : Constructs} (s : ConstantScope) (fixed : Option IntegerType) (written : Bool) (n : NodeId) (x : DeclId) (v : Int) (rest : List Enumerator) : CheckResult L (List (DeclId * Int))

One enumeration constant x with its value v (at the node n; written as for Program.outOfRange), then the rest, in the scope s, fitting int or the fixed underlying type.

cfamily.Program.constantOf

def Program.constantOf (s : ConstantScope) (x : DeclId) (t : TypeSyntax) (init : Option Init) : Option Int

The value of the variable x of the written type t with the initializer init as a constant, in the scope s: where the rules make const integral variables constants, a const integer type initialized with an integer constant expression, converted to the type (a floating one truncated; ConstantScope.with).

cfamily.Program.expanded

def Program.expanded (typedefs : List (String * TypeSyntax)) (fuel : Nat) (t : TypeSyntax) : TypeSyntax

The written type t with the names of the typedefs replaced by the types they stand for, everywhere in it (fuel: at most the number of typedefs, which bounds their chains).

cfamily.Program.sameType

def Program.sameType (typedefs : List (String * TypeSyntax)) (a : TypeSyntax) (b : TypeSyntax) : Bool

Whether two written types a and b are the same type, through the typedefs: a typedef may be defined again as the same type (C11 6.7p3, C++ [dcl.typedef]p3), not as another.

cfamily.Program.writtenName

def Program.writtenName (x : String) : String

The name a typedef is written with: a block’s is moved to file scope as x#n (cfamily.statics).

cfamily.Program.typeNames

def Program.typeNames {L : Constructs} (rules : Rules) (target : Target) (names : TypeNames) (items : List Item) : CheckResult L TypeNames

The type names of the items added to names, in order: typedefs (each once), enums (unsigned int if no constant is negative, else int, as clang), the constants (with const integral variables where the dialect’s rules allow, Program.constantOf), their values computed on the target.

cfamily.ProgramDialect.parameterType

def ProgramDialect.parameterType {L : Constructs} (pd : ProgramDialect L) (g : Globals L) (n : NodeId) (t : TypeSyntax) : CheckResult L (Ty L)

A parameter’s type: an array is adjusted to a pointer to its element (C11 6.7.6.3p7), then the dialect’s way of passing it.

cfamily.ProgramDialect.parameters

def ProgramDialect.parameters {L : Constructs} (pd : ProgramDialect L) (g : Globals L) (n : NodeId) (ps : List Param) : CheckResult L (List (DeclId * Ty L))

The parameters of a function with their types, in order.

cfamily.ProgramDialect.resultType

def ProgramDialect.resultType {L : Constructs} (pd : ProgramDialect L) (g : Globals L) (n : NodeId) (r : Option TypeSyntax) : CheckResult L (Option (Ty L))

A function’s result type (none is void).

cfamily.ProgramDialect.defaultOf

def ProgramDialect.defaultOf {L : Constructs} (pd : ProgramDialect L) (g : Globals L) (env : Env L) (n : NodeId) (t : Ty L) (d : Option Expr) : CheckResult L (Option (DefaultArgument L))

A parameter’s default argument checked in the scope of the globals: a constant if it needs nothing first, else evaluated at each call ([dcl.fct.default]p9).

cfamily.ProgramDialect.defaults

def ProgramDialect.defaults {L : Constructs} (pd : ProgramDialect L) (g : Globals L) (env : Env L) (n : NodeId) (ps : List Param) (ts : List (DeclId * Ty L)) : CheckResult L (List (Defaulted L))

The default arguments of the parameters, in order.

cfamily.ProgramDialect.signatureOf

def ProgramDialect.signatureOf {L : Constructs} (pd : ProgramDialect L) (g : Globals L) (env : Env L) (withDefaults : Bool) (f : FunctionDefinition) : CheckResult L (Signature L)

A function’s signature; its defaults checked in the tables g (none when withDefaults is false).

cfamily.ProgramDialect.signaturesFrom

def ProgramDialect.signaturesFrom {L : Constructs} (pd : ProgramDialect L) (g : Globals L) (env : Env L) (withDefaults : Bool) (done : List (Signature L)) (fs : List FunctionDefinition) : CheckResult L (List (Signature L))

The signatures of the functions after those done (kept in reverse), in order: a loop over the functions (the library’s are hundreds), not one level of recursion per function.

cfamily.ProgramDialect.signatures

def ProgramDialect.signatures {L : Constructs} (pd : ProgramDialect L) (g : Globals L) (env : Env L) (withDefaults : Bool) (fs : List FunctionDefinition) : CheckResult L (List (Signature L))

The signatures of the functions, in order.

cfamily.ProgramDialect.globalTypes

def ProgramDialect.globalTypes {L : Constructs} (pd : ProgramDialect L) (g : Globals L) (env : Env L) (items : List Item) : CheckResult L (Env L)

The globals with their declared types, the last first (the environment defaults are checked in: a default may use a global, read when the call is made, [dcl.fct.default]p9).

cfamily.ProgramDialect.signaturesInOrder

def ProgramDialect.signaturesInOrder {L : Constructs} (pd : ProgramDialect L) (g : Globals L) (env : Env L) (firsts : SearchTree Nat Unit) (position : Nat) (done : List (Signature L)) (fs : List FunctionDefinition) : CheckResult L (List (Signature L))

The signatures of the functions fs with their defaults, in order (those done kept in reverse), checked by the dialect pd in the file scope env: a function’s defaults are checked with the functions before it having theirs (a default may call a function declared before it, whose own defaults apply, [dcl.fct.default]p9). The signatures of g start as those without defaults; position is the next function’s position, and firsts are the positions of the functions that are the first of their name (the one a lookup by the name finds), whose entry takes the defaults once it has them.

cfamily.Stmt.initializes

def Stmt.initializes (s : Stmt) : Bool

Whether a statement (or its label’s) is a declaration with an initializer.

cfamily.Stmt.leadingLabels

def Stmt.leadingLabels (s : Stmt) : List String

The labels a statement starts with (a label’s statement may be a label too).

cfamily.Stmt.jumpPastFrom

def Stmt.jumpPastFrom (gs : List (String * NodeId)) (ss : List Stmt) (seen : Bool) : Option NodeId

A goto among gs to a label of the statements after a declaration with an initializer: the goto’s node.

cfamily.Item.headersIncluded

def Item.headersIncluded (items : List Item) : List String

The headers a program includes, as written.

cfamily.Ty.returnsValue

def Ty.returnsValue {L : Constructs} (r : Option (Ty L)) : Bool

Whether a function of the result type r returns a value (none, or void however it is written, does not).

cfamily.TypedStmt.endingWith

def TypedStmt.endingWith {L : Constructs} (rules : Rules) (n : NodeId) (returnsValue : Bool) (body : TypedStmt L) : TypedStmt L

A function’s checked body with what running off its end does: where the rules make it undefined for a function that returns a value (C++17 [stmt.return]p2; returnsValue is false for the entry, main, whose end returns 0), a stop at the function’s node n after the body’s last statement, inside its block (a return leaves before it); else the body as it is (C 6.9.1p12: the caller using the value reads an indeterminate one).

cfamily.ProgramDialect.undefinedTag

def ProgramDialect.undefinedTag {L : Constructs} (pd : ProgramDialect L) (g : Globals L) (written : TypeSyntax) (t : Ty L) : Bool

Whether the type written as a struct, union or class (const or not) is one the program only declares: its resolved type t, completed by the dialect pd with the globals g, is still known only by name. A dialect’s own type named that way (C++’s std::nullptr_t) is not written as a tag, so it is not one.

cfamily.ProgramDialect.undefinedParameter

def ProgramDialect.undefinedParameter {L : Constructs} (pd : ProgramDialect L) (g : Globals L) (ps : List Param) (ts : List (DeclId * Ty L)) : Bool

Whether one of the parameters, written (ps) and resolved (ts, in the same order), is of a struct, union or class type the program only declares (by the dialect pd with the globals g).

cfamily.ProgramDialect.incompleteInDefinition

def ProgramDialect.incompleteInDefinition {L : Constructs} (pd : ProgramDialect L) (g : Globals L) (ps : List Param) (parameters : List (DeclId * Ty L)) (r : Option TypeSyntax) (result : Option (Ty L)) : Option String

What is wrong with a function definition’s types (by the dialect pd with the globals g): a parameter (written ps, resolved parameters), or the result (written r, resolved result), of a struct, union or class type the program only declares (C11 6.9.1p3, p7; C++17 [dcl.fct.def.general]p2: a definition needs them complete, a declaration alone does not).

cfamily.ProgramDialect.function

def ProgramDialect.function {L : Constructs} (pd : ProgramDialect L) (g : Globals L) (genv : Env L) (f : FunctionDefinition) : CheckResult L (CheckedFunction L)

Checks a function: its parameters and result complete, its labels distinct, no jump past an initialization unless the rules allow it, the body with the parameters (then the globals) in scope.

cfamily.ProgramDialect.global

def ProgramDialect.global {L : Constructs} (pd : ProgramDialect L) (g : Globals L) (genv : Env L) (n : NodeId) (declaration : Stmt) : CheckResult L (TypedStmt L)

A global’s declaration: its initializer a constant (no effects, reading no variable, C11 6.7.9p4; taking an address is fine), zero without one; where the rules allow dynamic initialization, whatever the declaration runs (a constructor, a call; C++ [basic.start.dynamic]).

cfamily.FunctionDefinition.qualifier

def FunctionDefinition.qualifier (f : String) : Option String

The name of the class a function’s name f is qualified by (C::f names C, O::I::f names O::I), else none.

cfamily.ProgramDialect.atDefinition

def ProgramDialect.atDefinition {L : Constructs} (g : Globals L) (here : Globals L) (name : String) : Globals L

The globals a function definition named name is checked with: here, the globals g with only the struct, union and class types defined before it (C11 6.7.2.3p4: a tag’s type is incomplete until the end of its definition; C++17 [class.mem]p6), so its parameters, result and body see a type defined after it as incomplete; a member function of a class the program defines (named C::f) with g as it is: the tree keeps a member function in its class whether its definition is written there or after it ([class.mfct]p2), and one written inside sees the class complete ([class.mem]p6), so where it was written is not known.

cfamily.ProgramDialect.itemsFrom

def ProgramDialect.itemsFrom {L : Constructs} (pd : ProgramDialect L) (g : Globals L) (here : Globals L) (genv : Env L) (done : CheckedProgram L) (items : List Item) : CheckResult L (CheckedProgram L)

The items in order: a global is visible to the items after it. What is checked so far is kept in reverse (in done) and put in order at the end: the check goes through the items as a loop, not one level of recursion per item (the program’s items with the library’s are hundreds, and a kernel evaluating it would nest that deep). The dialect pd, the globals g, here (g with the struct and union types the items so far define, ProgramDialect.atDefinition), the globals in scope genv, what is checked so far done, and the items left.

cfamily.TypeEntry

def TypeEntry : Type

A struct, union or class type in the tables: its name and its members’ names and types.

cfamily.TypeEntry.isInstance

def TypeEntry.isInstance (t : TypeEntry) : Bool

Whether the type t is a class template’s instance: its name has template arguments (Box<int>).

cfamily.ProgramDialect.instances

def ProgramDialect.instances (types : List TypeEntry) : List TypeEntry

The class template instances among the types (a name with template arguments, Box<int>): one is instantiated where it is needed ([temp.inst]p2), so it is complete wherever it is used, before or after a function definition; a type the program defines by name is complete only after its definition (ProgramDialect.atDefinition).

cfamily.ProgramDialect.items

def ProgramDialect.items {L : Constructs} (pd : ProgramDialect L) (g : Globals L) (genv : Env L) (items : List Item) : CheckResult L (CheckedProgram L)

The items in order: a global is visible to the items after it. A function definition sees the class template instances from the start (an instance the program never writes, auto t = make_tuple(1, 2, 3), is made while checking and placed nowhere before it) and the other types once their definitions are passed.

cfamily.Item.globals

def Item.globals (items : List Item) : List (DeclId * TypeSyntax)

The globals of the items with their written types (for the effect summaries).

cfamily.ProgramDialect.mainParameters

def ProgramDialect.mainParameters {L : Constructs} (pd : ProgramDialect L) (ps : List (Ty L)) : Bool

Whether main’s parameters are none, or argc and argv (int, char **; C11 5.1.2.2.1p1).

cfamily.ProgramDialect.hasMain

def ProgramDialect.hasMain {L : Constructs} (pd : ProgramDialect L) (g : Globals L) : Bool

Whether the program has int main(void) or int main(int argc, char *argv[]).

cfamily.ProgramDialect.hasEntry

def ProgramDialect.hasEntry {L : Constructs} (pd : ProgramDialect L) (g : Globals L) : Bool

Whether the program has its entry: main as C and C++ require it, another (a board core’s app_main) as void f(void).

cfamily.ProgramDialect.missingEntry

def ProgramDialect.missingEntry {L : Constructs} (pd : ProgramDialect L) : String

Why a program without its entry is rejected (another entry is the core’s: GCC’s linker names it).

cfamily.Program.addressedFunctions

def Program.addressedFunctions (items : List Item) : Option (List String)

The functions whose address the items take (f as a value), none when a member function’s address is taken (a call through a member pointer may call any member function).

cfamily.HoleTypes

def HoleTypes : Type

The type query’s holes and the types they stand for (none in ordinary checking).

cfamily.ProgramDialect.effectsOf

def ProgramDialect.effectsOf {L : Constructs} (pd : ProgramDialect L) (items : List Item) : EffectTable

The effect summaries of the items’ functions (with the dialect’s own, like C++’s methods).

cfamily.ProgramDialect.withLibraryCode

def ProgramDialect.withLibraryCode {L : Constructs} (pd : ProgramDialect L) (items : List Item) : List Item

The items with the library’s C functions the program uses, checking the comparators whose calls change nothing a run shows (cfamily.librarycode); the summaries are computed only for a program that needs the library’s code.

cfamily.Item.variableLengthIn

def Item.variableLengthIn (it : Item) : Option (NodeId * String)

Where an object or member of a type with an array whose length is not a constant (cfamily.lengths) may not be, in an item: at file scope or static (a variable length array has automatic storage only, C11 6.7.6.2p2; C++ [dcl.array]p1 has no variable length arrays, and GNU’s extension only in blocks), a struct’s or union’s member (C11 6.7.2.1p9: its length is a constant).

cfamily.Item.variableLengthMisplaced

def Item.variableLengthMisplaced (items : List Item) : Option (NodeId * String)

The first object or member of the items where a variable length array may not be (Item.variableLengthIn).

cfamily.ProgramDialect.checkItems

def ProgramDialect.checkItems {L : Constructs} (pd : ProgramDialect L) (n : NodeId) (query : HoleTypes) (source : NodeId -> Bool) (items : List Item) : CheckResult L (CheckedProgram L)

Checks prepared items once: the tables, main, the items.

cfamily.FunctionDefinition.tag

def FunctionDefinition.tag (f : FunctionDefinition) : NodeId * String

A function’s node and name.

cfamily.ProgramDialect.functionsChecked

def ProgramDialect.functionsChecked {L : Constructs} (pd : ProgramDialect L) (g : Globals L) (fs : List (Env L * FunctionDefinition)) : CheckResult L (List (CheckedFunction L))

Deferred functions checked, each with the globals before it.

cfamily.Reached

record Reached (L : Constructs)

A body checked, with where what it uses comes from: none for the program’s own (each use is its statement’s), else the node in the program a deferred function was first used at (what a library function uses is the program’s use).

cfamily.Reached.of

def Reached.of {L : Constructs} (origin : Option NodeId) (body : TypedStmt L) : Reached L

A body reached from a node (none: the program’s own).

cfamily.Reached.uses

def Reached.uses {L : Constructs} (r : Reached L) : List (String * NodeId)

The functions a body uses, each with the node it counts as used at.

cfamily.CheckResult.placed

def CheckResult.placed {L : Constructs} {A : Type} (source : NodeId -> Bool) (origin : Option NodeId) (r : CheckResult L A) : CheckResult L A

A rejection (or a construct the model does not provide) placed in the program: one at a node the program does not have (in a library’s function, checked because the program used it) is placed at the node it was used at.

cfamily.ProgramDialect.reachedChecked

def ProgramDialect.reachedChecked {L : Constructs} (pd : ProgramDialect L) (g : Globals L) (source : NodeId -> Bool) (originOf : Env L * FunctionDefinition -> Option NodeId) (ds : List (Env L * FunctionDefinition)) : CheckResult L (List (CheckedFunction L * Option NodeId))

Deferred functions checked, each with the node it was first used at (its rejection placed there).

cfamily.ProgramDialect.using

def ProgramDialect.using {L : Constructs} (pd : ProgramDialect L) (g : Globals L) (source : NodeId -> Bool) (genv : Env L) (fuel : Nat) (fresh : List (Reached L)) (c : CheckedProgram L) : CheckResult L (CheckedProgram L)

A checked program with the deferred functions it uses checked (a dialect’s function checked only if used, ProgramExtension.lazy): those the bodies just checked call or take the address of, then those these do, until no more are used; one that does not check is the program’s failure.

cfamily.CheckedProgram.completed

def CheckedProgram.completed {L : Constructs} (pd : ProgramDialect L) (g : Globals L) (source : NodeId -> Bool) (genv : Env L) (c : CheckedProgram L) : CheckResult L (CheckedProgram L)

A checked program with the deferred functions it uses checked.

cfamily.ProgramDialect.instanceRounds

def ProgramDialect.instanceRounds : Nat

How many rounds of instances’ definitions checking a program may take (an instance’s body may need another’s).

cfamily.ProgramDialect.newInstances

def ProgramDialect.newInstances {L : Constructs} (pd : ProgramDialect L) (g : Globals L) (genv : Env L) (c : CheckedProgram L) (uses : List (String * NodeId)) : List (Env L * FunctionDefinition)

The instances the uses name that the program has no function or deferred function for, each made from its template once (ProgramExtension.instantiate), with the globals’ scope.

cfamily.ProgramDialect.checkAnswering

def ProgramDialect.checkAnswering {L : Constructs} (pd : ProgramDialect L) (fuel : Nat) (query : HoleTypes) (source : NodeId -> Bool) (program : Program) : CheckResult L (CheckedProgram L)

Checks a program: the dialect’s passes, the library’s C functions it uses, then the items; a request of the dialect is answered by adding items to the program, which is prepared and checked again (at most fuel times).

cfamily.ProgramDialect.requestFuel

def ProgramDialect.requestFuel : Nat

The number of times checking may start again for the dialect’s requests (each a function template’s instance or a lambda’s deduced result type in C++; a program with a few of each needs more than a dozen).

cfamily.Program.checkWith

def Program.checkWith {L : Constructs} (pd : ProgramDialect L) (query : HoleTypes) (program : Program) : CheckResult L (CheckedProgram L)

Checks a program with the type query’s holes or without: a name declared twice in one block scope rejected, the names written resolved by the scopes, then the dialect’s passes, the library’s C functions it uses, then the items.

cfamily.Program.check

def Program.check {L : Constructs} (pd : ProgramDialect L) (program : Program) : CheckResult L (CheckedProgram L)

Checks a program.

cfamily.Program.checkCollecting

def Program.checkCollecting {L : Constructs} (pd : ProgramDialect L) (holes : List (NodeId * TypeSyntax)) (program : Program) : CheckResult L (CheckedProgram L)

Checks a program for the type query: each hole stands for a value of the type given for it, and a statement that does not check is recorded (checkError) while checking goes on.