tables

cfamily.DefaultArgument

data DefaultArgument (L : Constructs)

A parameter’s default argument: a constant expression, or one evaluated at each call with the statements it needs first ([dcl.fct.default]p9).

cfamily.Defaulted

def Defaulted (L : Constructs) : Type

A parameter’s default argument, if it has one.

cfamily.Signature

record Signature (L : Constructs)

A function’s signature: name, parameter types, result (none is void), and each parameter’s default.

cfamily.Signature.of

def Signature.of {L : Constructs} (name : String) (parameters : List (Ty L)) (result : Option (Ty L)) (defaults : List (Defaulted L)) : Signature L

A signature from its parts.

cfamily.TypeNames

record TypeNames

The names of types: typedefs (name to written type), enums (name to underlying type; an anonymous one named after its node), enumeration constants (declaration to value), the enum each constant belongs to, whether an enumeration is a type of its own (the dialect’s Rules.enumerationIsDistinct), and the scoped enumerations (C++’s enum class).

cfamily.TypeNames.empty

def TypeNames.empty : TypeNames

No typedefs, enums or constants.

cfamily.TypeNames.typeOfEnum

def TypeNames.typeOfEnum {L : Constructs} (names : TypeNames) (p : Platform) (x : String) : Option (Ty L)

The type an enum’s name is: an enumeration type of its own (an unscoped one promoting to int: each constant fits int, C++ [conv.prom]p3; a scoped one does not promote, [conv.prom]p4, and takes part as itself), or its underlying integer type where enumerations are not distinct (C 6.7.2.2p4).

cfamily.TypeNames.enumeratorType

def TypeNames.enumeratorType {L : Constructs} (names : TypeNames) (p : Platform) (x : DeclId) : Option (Ty L)

The enumeration type of an enumeration constant, where enumerations are distinct (C++ [dcl.enum]p5).

cfamily.Effects

record Effects

What a function may do, conservatively (it may say more than happens, never less): input or output, the globals it writes and reads, whether it writes or reads memory elsewhere (through pointers or references), and whether it writes or reads the object it is called on (in a dialect with member functions).

cfamily.SearchTree

data SearchTree (K : Type) (V : Type)

A search tree: a leaf, or an entry between the subtree of the smaller keys and that of the larger ones. Built from entries sorted by key (SearchTree.ofSorted) it is balanced: a lookup compares a number of keys logarithmic in the size, where a list of the entries compares each one (an Arduino board’s core has hundreds of functions).

cfamily.SearchTree.named

def SearchTree.named {V : Type} (t : SearchTree String V) (k : String) : Option V

The value of the name k in the tree t ordered by name, if it has one. (A lookup for each type of key: one that takes the comparison as an argument takes twice the steps.)

cfamily.SearchTree.atPosition

def SearchTree.atPosition {V : Type} (t : SearchTree Nat V) (i : Nat) : Option V

The value of the position i in the tree t ordered by position, if it has one.

cfamily.SearchTree.prefix

def SearchTree.prefix {K : Type} {V : Type} (fuel : Nat) (count : Nat) (entries : List (K * V)) : SearchTree K V * List (K * V)

The balanced tree of the first count entries (sorted by key) and the entries after them; fuel only bounds the recursion for the termination checker.

cfamily.SearchTree.replacedNamed

def SearchTree.replacedNamed {V : Type} (t : SearchTree String V) (k : String) (v : V) : SearchTree String V

The tree t with the value of the name k (which it has) replaced by v: the same shape.

cfamily.SearchTree.ofSorted

def SearchTree.ofSorted {K : Type} {V : Type} (entries : List (K * V)) : SearchTree K V

The balanced tree of the entries, sorted by key.

cfamily.SearchTree.numbered

def SearchTree.numbered {A : Type} (xs : List A) : List (Nat * A)

Each element of xs with its position.

cfamily.SearchTree.byPosition

def SearchTree.byPosition {A : Type} (xs : List A) : SearchTree Nat A

The elements of the list xs by position.

cfamily.SearchTree.firstOfEachName

def SearchTree.firstOfEachName {V : Type} (sorted : List (String * V)) : List (String * V)

The entries, sorted by name, with only the first of each name kept.

cfamily.SearchTree.firstByName

def SearchTree.firstByName {V : Type} (entries : List (String * V)) : SearchTree String V

The entries by name, the first of each name (as a list searched from its start finds it).

cfamily.SearchTree.firstPositions

def SearchTree.firstPositions (names : List String) : SearchTree Nat Unit

The positions of the names that are the first of their name in the list of names.

cfamily.SearchTree.values

def SearchTree.values {K : Type} {V : Type} (t : SearchTree K V) : List V

The values of the tree t, in the order of its keys.

cfamily.NameSet.of

def NameSet.of (names : List String) : SearchTree String Unit

The names as a set (a tree of them).

cfamily.NameSet.has

def NameSet.has (s : SearchTree String Unit) (x : String) : Bool

Whether the set s has the name x.

cfamily.FunctionsNamed

record FunctionsNamed

The functions of an effect table a key names, by their positions in the table (ascending): whether one has it as its name (the program defines it), those whose name or short name it is, and those whose short name it is.

cfamily.EffectTable

record EffectTable

The effect summaries: the globals, the variables whose elements are elsewhere (pointers, references, array parameters: subscripting them is elsewhere), the variables that are themselves elsewhere (references), the variables declared as arrays of a written length (their elements are their own storage), the functions of each key (a function’s keys are its name before the parameter list and its last part, by position), each function’s summary in order (and by position), and the functions a call through a pointer may call (those whose address the program takes; none when it may call anything: a member function’s address or a function the program does not define is taken). The names are trees, built once for a table, because each call’s summary is looked up by name in each round of the fixed point.

cfamily.EffectTable.empty

def EffectTable.empty : EffectTable

No effect summaries.

cfamily.Globals

record Globals (L : Constructs)

What checking a function knows about the program. query is none in ordinary checking; in the type query’s collect mode it holds the type each hole stands for. function is the name of the function being checked (empty for the globals): a dialect’s rules may depend on it (C++’s access control, inside a class’s member functions). target is what the program runs on (the dialect’s: an Arduino board’s integer widths for C++). headers are the headers the program includes, as written (limits.h, climits).

cfamily.Globals.lookup

def Globals.lookup {A : Type} (xs : List (String * A)) (key : String) : Option A

The first entry with the key, if any.

cfamily.Globals.signatureOf

def Globals.signatureOf {L : Constructs} (g : Globals L) (f : String) : Option (Signature L)

The signature of the function with the name, if any.

cfamily.Signatures.of

def Signatures.of {L : Constructs} (signatures : List (Signature L)) : SearchTree String (Signature L)

The signatures by name (the first of a name, when the list has more than one).

cfamily.Globals.structNamed

def Globals.structNamed {L : Constructs} (g : Globals L) (x : String) : Option (List (String * TypeSyntax))

The members of the struct with the name, as written.

cfamily.Globals.unionNamed

def Globals.unionNamed {L : Constructs} (g : Globals L) (x : String) : Option (List (String * TypeSyntax))

The members of the union with the name, as written (struct and union tags share one name space, C11 6.2.3).

cfamily.Globals.collects

def Globals.collects {L : Constructs} (g : Globals L) : Bool

Whether checking collects errors and goes on (the type query) instead of stopping at the first one.

cfamily.Globals.holeType

def Globals.holeType {L : Constructs} (g : Globals L) (n : NodeId) : Option TypeSyntax

In the type query, the type a hole stands for.

cfamily.LibraryType.integerHeaders

def LibraryType.integerHeaders : List String

The headers that declare the integer types of <stdint.h> and their limits (C11 7.8p1: <inttypes.h> includes it).

cfamily.LibraryType.sizeHeaders

def LibraryType.sizeHeaders : List String

The headers that declare size_t (C11 7.19, 7.21.1, 7.22, 7.24.1, 7.27.1, 7.28, 7.29.1).

cfamily.LibraryType

record LibraryType

A type a standard header names: its name, the headers that declare it and the integer type it is on a platform.

cfamily.LibraryType.exactly

def LibraryType.exactly (w : Nat) (p : Platform) : IntegerType

intN_t on a platform, as int where no type is N bits wide (none of the platforms modeled lacks one).

cfamily.LibraryType.unsignedExactly

def LibraryType.unsignedExactly (w : Nat) (p : Platform) : IntegerType

uintN_t on a platform.

cfamily.LibraryType.ofWidth

def LibraryType.ofWidth (w : Nat) : List LibraryType

intN_t, uintN_t, int_leastN_t and uint_leastN_t for a width (the least types are the exact ones on every platform modeled).

cfamily.LibraryType.standard

def LibraryType.standard : List LibraryType

The integer types the standard headers name.

cfamily.LibraryType.named

def LibraryType.named (name : String) : Option LibraryType

The type a standard header names, written with or without std::.

cfamily.LibraryType.includedAny

def LibraryType.includedAny {L : Constructs} (g : Globals L) (headers : List String) : Bool

Whether the program includes one of some headers.