expressions

cfamily.Env

def Env (L : Constructs) : Type

The local variables in scope: each declaration with its type, the innermost first.

cfamily.Statements

def Statements (L : Constructs) : Type

The statements a check makes, in order.

cfamily.Env.lookup

def Env.lookup {L : Constructs} (env : Env L) (x : DeclId) : Option (Ty L)

The type of a variable in scope, if it is.

cfamily.Mismatch

data Mismatch

What a call whose arguments match no function means: the program’s error (rejected, with the reason) or a function the model does not have in that form (a library’s class modeled without that overload: the program may be right, so it is not provided, never rejected).

cfamily.Checker

record Checker (L : Constructs)

The core’s checking functions, for a dialect checking its own syntax: an expression, an lvalue, expressions unsequenced with one another, and an expression against an expected type (malloc’s result takes its type from it).

cfamily.ExpressionExtension

record ExpressionExtension (L : Constructs)

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

• expression, lvalue: its own syntax (C++’s member calls, new, iostream), with the core’s checker;
• call: a function it adds by name (std::max, Arduino’s digitalWrite), before the program’s and the C library’s;
• unary, binary, assign: operators whose checked operands are of its types (C++’s std::string +, a class’s operators and operator=);
• index, member: subscripts and members of its types (a std::vector, a class with access control and bases);
• variableUse: the expression a variable of its type designates (a reference designates what it refers to);
• callResult: the expression a call’s result is, for its types (a function returning a reference);
• memberUse: the expression a member of its types designates (a member of reference type, what it refers to);
• isLvalue: which of its expressions are lvalues;
• against: an expression checked against an expected type it gives meaning to (C++’s overloaded function name, whose function is the one of the target’s type, [over.over]);
• mismatch: what a call of a function (by name) whose arguments do not match its parameters (too few, too many, one that does not convert) means, instead of the core’s reason (C++’s overload resolution finds no viable function, even with one candidate; a library class’s member not modeled in that form is not provided).

cfamily.ExpressionExtension.empty

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

The extension of a dialect without constructs of its own.

cfamily.CheckDialect

record CheckDialect (L : Constructs)

What checking expressions needs of a dialect: its name (in rejections), the target, the rules, the C library, and the extensions of types, conversions, effects and expressions.

cfamily.CheckDialect.platform

def CheckDialect.platform {L : Constructs} (d : CheckDialect L) : Platform

The platform of a dialect’s target.

cfamily.Ty.visibleMembers

def Ty.visibleMembers {L : Constructs} (fs : List (FieldTy L)) : List String

The visible members of a type (not a base’s or the dynamic type’s parts, named with #).

cfamily.CheckDialect.notPart

def CheckDialect.notPart {L : Constructs} {A : Type} (d : CheckDialect L) (n : NodeId) (what : String) : CheckResult L A

A rejection: the construct is not part of the dialect.

cfamily.Rules.undeclaredLibraryName

def Rules.undeclaredLibraryName {L : Constructs} {A : Type} (rules : Rules) (g : Globals L) (n : NodeId) (name : String) (headers : List String) : CheckResult L A

A name a standard header declares, used without including that header: undeclared, unless the dialect’s headers may include the others and the program includes some (then whether it is declared depends on the library).

cfamily.TypeSyntax.hiddenLibraryType

def TypeSyntax.hiddenLibraryType {L : Constructs} (g : Globals L) (t : TypeSyntax) : Option LibraryType

The type a standard header names that the written type t uses without the program including the header (the headers included are those in g), if any.

cfamily.TypeSyntax.hasVariableLength

def TypeSyntax.hasVariableLength (t : TypeSyntax) : Bool

Whether the written type t has an array whose length is still an expression: not a constant (cfamily.lengths).

cfamily.CheckDialect.resolve

def CheckDialect.resolve {L : Constructs} (d : CheckDialect L) (g : Globals L) (n : NodeId) (t : TypeSyntax) : CheckResult L (Ty L)

A written type resolved and completed, or rejected at the node. A variable length array’s type where the model has none (it has one only as a block’s declaration, sDeclV) is not decided.

cfamily.CheckDialect.complete

def CheckDialect.complete {L : Constructs} (d : CheckDialect L) (g : Globals L) (t : Ty L) : Ty L

A type completed.

cfamily.CheckDialect.rvalue

def CheckDialect.rvalue {L : Constructs} (d : CheckDialect L) (e : TypedExpr L) : TypedExpr L

The value of a typed expression (arrays decay).

cfamily.CheckDialect.typeOf

def CheckDialect.typeOf {L : Constructs} (d : CheckDialect L) (e : TypedExpr L) : Ty L

The type of a typed expression.

cfamily.CheckDialect.int

def CheckDialect.int {L : Constructs} (d : CheckDialect L) : IntegerType

The int type of the dialect’s target.

cfamily.CheckDialect.readsOf

def CheckDialect.readsOf {L : Constructs} (d : CheckDialect L) (lv : TypedExpr L) : List (MemoryAccess L)

The reads of the value of the lvalue lv, by what the dialect d counts as an lvalue on its target.

cfamily.Ty.knownOnlyByName

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

Whether the type t is a struct or class known only by name (declared, never defined; after CheckDialect.complete): an lvalue of it may be designated (*p, &*p), not read or have its members accessed.

cfamily.Ty.hasIncomplete

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

Whether a type has an incomplete part (not behind a pointer): a struct known only by name, void, an array of unknown length.

cfamily.Ty.anyIncomplete

def Ty.anyIncomplete {L : Constructs} (fs : List (FieldTy L)) : Bool

Whether a member has an incomplete type.

cfamily.Ty.members

def Ty.members {L : Constructs} (t : Ty L) : Option (List (FieldTy L))

The members of a struct or union type, if it is one.

cfamily.Ty.functionPointer

def Ty.functionPointer {L : Constructs} (t : Ty L) : Option (List (Ty L) * Option (Ty L))

The parameter and result types of a function pointer type, if it is one.

cfamily.TypedStmt.storing

def TypedStmt.storing {L : Constructs} (n : NodeId) (lv : TypedExpr L) (v : TypedExpr L) : TypedStmt L

The value stored by an assignment of v to the lvalue lv.

cfamily.Lifted.writable

def Lifted.writable {L : Constructs} (n : NodeId) (l : Lifted L) : CheckResult L Unit

A rejection unless the lvalue may be written: a const object cannot (C11 6.5.16p2).

cfamily.Effects.writeAccesses

def Effects.writeAccesses {L : Constructs} (e : Effects) : List (MemoryAccess L)

The accesses a call makes: the callee’s effects, as input or output, the globals it touches, memory elsewhere.

cfamily.Effects.readAccesses

def Effects.readAccesses {L : Constructs} (e : Effects) : List (MemoryAccess L)

The reads a call makes.

cfamily.CheckDialect.receiverAccesses

def CheckDialect.receiverAccesses {L : Constructs} (r : TypedExpr L) : List (MemoryAccess L)

The accesses a call makes to its receiver, the object whose address is its first argument: a variable’s, else memory elsewhere.

cfamily.CheckDialect.calleeEffects

def CheckDialect.calleeEffects {L : Constructs} (d : CheckDialect L) (g : Globals L) (f : String) (args : List (TypedExpr L)) : Effects

The effects of calling the function named f: the program’s summary, or the library’s.

cfamily.Lifted.withExpr

def Lifted.withExpr {L : Constructs} (a : Lifted L) (e : TypedExpr L) : Lifted L

The lifted expression with another expression, its statements and accesses kept.

cfamily.Lifted.reading

def Lifted.reading {L : Constructs} (e : TypedExpr L) (reads : List (MemoryAccess L)) : Lifted L

An expression that needs nothing first and makes the reads.

cfamily.CheckDialect.pure

def CheckDialect.pure {L : Constructs} (e : TypedExpr L) : CheckResult L (Lifted L)

A literal or other expression that needs nothing first.

cfamily.CheckDialect.libraryConstant

def CheckDialect.libraryConstant {L : Constructs} (d : CheckDialect L) (g : Globals L) (n : NodeId) (name : String) : CheckResult L (Lifted L)

A macro constant of the standard headers (eConst), when the program includes a header that declares it; otherwise the name is undeclared (C11 6.5.1p2: an identifier is a primary expression only if declared).

cfamily.Rules.libraryConstant

def Rules.libraryConstant {L : Constructs} (rules : Rules) (g : Globals L) (n : NodeId) (name : String) : CheckResult L (Lifted L)

A macro constant under a dialect’s rules: its value when the program includes a header that declares it.

cfamily.CheckDialect.integerLiteral

def CheckDialect.integerLiteral {L : Constructs} (d : CheckDialect L) (n : NodeId) (v : Int) : CheckResult L (Lifted L)

A decimal integer constant: int, long or long long, the first that holds it.

cfamily.CheckDialect.writtenInteger

def CheckDialect.writtenInteger {L : Constructs} (d : CheckDialect L) (n : NodeId) (v : Int) (suffix : String) (decimal : Bool) : CheckResult L (Lifted L)

An integer constant written with a suffix or not in decimal: its type by C11 6.4.4.1p5.

cfamily.Literal.isLongDouble

def Literal.isLongDouble (text : String) : Bool

Whether a floating constant’s text ends in the suffix l or L (a long double, C11 6.4.4.2p4).

cfamily.CheckDialect.floatLiteral

def CheckDialect.floatLiteral {L : Constructs} (d : CheckDialect L) (n : NodeId) (text : String) (single : Bool) : CheckResult L (Lifted L)

A floating constant as written: float with the f suffix (single), long double when the text ends in l or L (the digits before it read in long double’s format), else double.

cfamily.CheckDialect.stringOf

def CheckDialect.stringOf {L : Constructs} (d : CheckDialect L) (n : NodeId) (str : String) : CheckResult L (Lifted L)

A string literal: an array of char (const char by the rules) with room for the null.

cfamily.CheckDialect.wideStringOf

def CheckDialect.wideStringOf {L : Constructs} (d : CheckDialect L) (n : NodeId) (str : String) : CheckResult L (Lifted L)

A wide string literal: an array of wchar_t (int on LP64), one element per code point and the null.

cfamily.CheckDialect.characterLiteral

def CheckDialect.characterLiteral {L : Constructs} (d : CheckDialect L) (n : NodeId) (c : Nat) : CheckResult L (Lifted L)

A character constant: of type char or int by the rules.

cfamily.CheckDialect.truth

def CheckDialect.truth {L : Constructs} (d : CheckDialect L) : IntegerType

The type of a truth value (a comparison’s, true’s) in the dialect d: bool or int by its rules.

cfamily.CheckDialect.booleanLiteral

def CheckDialect.booleanLiteral {L : Constructs} (d : CheckDialect L) (n : NodeId) (b : Bool) : CheckResult L (Lifted L)

true or false: of the truth type.

cfamily.CheckDialect.variableExpr

def CheckDialect.variableExpr {L : Constructs} (d : CheckDialect L) (n : NodeId) (t : Ty L) (x : DeclId) : TypedExpr L

The expression a variable designates: the dialect’s (a reference), or the variable itself.

cfamily.CheckDialect.variableLvalue

def CheckDialect.variableLvalue {L : Constructs} (d : CheckDialect L) (env : Env L) (n : NodeId) (x : DeclId) : CheckResult L (Lifted L)

A variable used as an lvalue: a local or global in scope; an enumeration constant is not an lvalue.

cfamily.CheckDialect.variableValue

def CheckDialect.variableValue {L : Constructs} (d : CheckDialect L) (g : Globals L) (env : Env L) (n : NodeId) (x : DeclId) : CheckResult L (Lifted L)

A variable’s value: a variable in scope (read), or an enumeration constant (an int constant, C11 6.4.4.3p2).

cfamily.CheckDialect.hole

def CheckDialect.hole {L : Constructs} (d : CheckDialect L) (g : Globals L) (n : NodeId) : CheckResult L (Lifted L)

A hole of the type query: a value of the type it stands for; outside the query an empty slot.

cfamily.CheckDialect.unary

def CheckDialect.unary {L : Constructs} (d : CheckDialect L) (g : Globals L) (n : NodeId) (op : UnaryOp) (a : Lifted L) : CheckResult L (Lifted L)

A unary operator on a checked operand: the dialect’s for its types, else the core’s.

cfamily.CheckDialect.shortCircuit

def CheckDialect.shortCircuit {L : Constructs} (d : CheckDialect L) (n : NodeId) (op : BinaryOp) (a : Lifted L) (b : Lifted L) : Lifted L

&& and || whose right side needs statements first: the right side runs only when needed, its value in a temporary named for the node, of the truth type (C11 6.5.13p4, 6.5.14p4; C++ [expr.log.and]p1).

cfamily.CheckDialect.binary

def CheckDialect.binary {L : Constructs} (d : CheckDialect L) (g : Globals L) (n : NodeId) (op : BinaryOp) (a : Lifted L) (b : Lifted L) : CheckResult L (Lifted L)

A binary operator on checked operands: the dialect’s for its types; && and || short-circuit; else both operands unsequenced (C11 6.5p2) and the core’s typing.

cfamily.CheckDialect.assignLifted

def CheckDialect.assignLifted {L : Constructs} (d : CheckDialect L) (g : Globals L) (n : NodeId) (t : Ty L) (e : TypedExpr L) : CheckResult L (Lifted L)

e converted to t as if by assignment: the dialect’s own conversions first (with the statements they need first, a temporary a const reference binds to), else the core’s.

cfamily.CheckDialect.assignTo

def CheckDialect.assignTo {L : Constructs} (d : CheckDialect L) (g : Globals L) (n : NodeId) (t : Ty L) (e : TypedExpr L) : CheckResult L (TypedExpr L)

e converted to t as if by assignment where nothing can run first (an assignment’s value, a conditional’s operands): a conversion that needs a temporary is rejected.

cfamily.CheckDialect.assignedValue

def CheckDialect.assignedValue {L : Constructs} (d : CheckDialect L) (g : Globals L) (n : NodeId) (lv : TypedExpr L) (op : Option BinaryOp) (e : TypedExpr L) : CheckResult L (TypedExpr L)

The value an assignment stores: e converted to the lvalue’s type; for op=, lv op e converted back.

cfamily.CheckDialect.assignment

def CheckDialect.assignment {L : Constructs} (d : CheckDialect L) (g : Globals L) (n : NodeId) (op : Option BinaryOp) (l : Lifted L) (a : Lifted L) : CheckResult L (Lifted L)

An assignment of a checked right side to a checked lvalue: the dialect’s for its types (operator=), else the value stored after both sides; the value of the expression is the lvalue (C11 6.5.16p3). Where the right side goes first (C++17), it does, its value kept in a temporary when the left side has statements of its own.

cfamily.CheckDialect.increment

def CheckDialect.increment {L : Constructs} (d : CheckDialect L) (g : Globals L) (n : NodeId) (inc : Bool) (post : Bool) (l : Lifted L) : CheckResult L (Lifted L)

++ or – on a checked lvalue: prefix gives the lvalue after the change, postfix the value before it (kept in a temporary named for the node).

cfamily.CheckDialect.incremented

def CheckDialect.incremented {L : Constructs} (d : CheckDialect L) (g : Globals L) (n : NodeId) (inc : Bool) (post : Bool) (l : Lifted L) : CheckResult L (Lifted L)

++ or – of an lvalue whose type may be incremented.

cfamily.CheckDialect.indirection

def CheckDialect.indirection {L : Constructs} (d : CheckDialect L) (g : Globals L) (n : NodeId) (a : Lifted L) : CheckResult L (Lifted L)

The lvalue *p from a checked pointer: the pointed-to type complete, or a struct or class known only by name (the result is an lvalue, C11 6.5.3.2p4, C++17 [expr.unary.op]p1; reading it or a member is what needs the type complete, CheckDialect.indirectValue, CheckDialect.memberOf).

cfamily.CheckDialect.subscript

def CheckDialect.subscript {L : Constructs} (d : CheckDialect L) (g : Globals L) (n : NodeId) (a : Lifted L) (i : Lifted L) : CheckResult L (Lifted L)

The lvalue a[i] (= *(a + i), C11 6.5.2.1p2) from checked operands: the dialect’s for its types, else a pointer and an integer, either way round (i[a] is *(i + a), the same lvalue; C++17 [expr.sub]p1 too), unsequenced.

cfamily.CheckDialect.pointerSubscript

def CheckDialect.pointerSubscript {L : Constructs} (d : CheckDialect L) (g : Globals L) (n : NodeId) (p : Lifted L) (k : Lifted L) : CheckResult L (Lifted L)

The lvalue *(p + k) from a checked pointer operand p (an array converted) and the other operand k, an integer.

cfamily.CheckDialect.memberOf

def CheckDialect.memberOf {L : Constructs} (d : CheckDialect L) (g : Globals L) (n : NodeId) (f : String) (a : Lifted L) : CheckResult L (Lifted L)

The member f of a checked lvalue of struct or union type: the dialect’s for its types, else by name, also inside an anonymous member (C11 6.7.2.1p13); a struct or class known only by name has no members to access (C11 6.5.2.3p1, C++17 [expr.ref]p4).

cfamily.CheckDialect.bindingPart

def CheckDialect.bindingPart {L : Constructs} (d : CheckDialect L) (g : Globals L) (n : NodeId) (k : Nat) (count : Nat) (a : Lifted L) : CheckResult L (Lifted L)

A structured binding’s k-th part of an object with count names: the k-th element of an array, the k-th visible member of a struct or class; a different number of parts than names is an error ([dcl.struct.bind]p3, p5).

cfamily.CheckDialect.reading

def CheckDialect.reading {L : Constructs} (d : CheckDialect L) (l : Lifted L) : Lifted L

A value with its reads added.

cfamily.CheckDialect.sizeOfType

def CheckDialect.sizeOfType {L : Constructs} (d : CheckDialect L) (g : Globals L) (n : NodeId) (t : Ty L) : CheckResult L (Lifted L)

sizeof a type: the size by the dialect’s layout, as size_t; an incomplete type has none.

cfamily.CheckDialect.sizeOfExpr

def CheckDialect.sizeOfExpr {L : Constructs} (d : CheckDialect L) (g : Globals L) (n : NodeId) (a : Lifted L) : CheckResult L (Lifted L)

sizeof an expression (not evaluated): a variable length array’s size at run time, else its type’s.

cfamily.CheckDialect.conditionalOf

def CheckDialect.conditionalOf {L : Constructs} (d : CheckDialect L) (g : Globals L) (n : NodeId) (c : Lifted L) (a : Lifted L) (b : Lifted L) : CheckResult L (Lifted L)

c ? a : b from checked operands: the type by C11 6.5.15; without effects in a or b the lazy conditional, else a temporary named for the node assigned in a branch (only one side runs).

cfamily.CheckDialect.evaluating

def CheckDialect.evaluating {L : Constructs} (d : CheckDialect L) (n : NodeId) (e : TypedExpr L) : TypedStmt L

Evaluating an expression’s value only for its undefined behavior.

cfamily.CheckDialect.afterDropped

def CheckDialect.afterDropped {L : Constructs} (d : CheckDialect L) (dropped : List (TypedStmt L)) (b : Lifted L) : Lifted L

a, b with a’s statements already made (its effects, Expr.droppedWithin): a sequence point, then b (C11 6.5.17: not an lvalue; C++ [expr.comma]p1: an lvalue when b is, by the rules).

cfamily.CheckDialect.convertAll

def CheckDialect.convertAll {L : Constructs} (d : CheckDialect L) (g : Globals L) (n : NodeId) (name : Option String) (ps : List (Ty L)) (es : List (TypedExpr L)) : CheckResult L (LiftedList L)

Arguments converted to the parameters’ types as if by assignment, with the statements the conversions need first (after the arguments’). Each is converted at its own node: a temporary a const reference binds to is named for the node, so two arguments bound that way (std::min(2, 5)) need two. Too few or too many are refused with the counts, and the function’s name when the call names one.

cfamily.CheckDialect.convertCounted

def CheckDialect.convertCounted {L : Constructs} (d : CheckDialect L) (g : Globals L) (n : NodeId) (tooFew : Refusal) (tooMany : Refusal) (ps : List (Ty L)) (es : List (TypedExpr L)) : CheckResult L (LiftedList L)

CheckDialect.convertAll (the dialect d, the program’s tables g, the call’s node n, the parameters’ types ps and the arguments es) with its refusals tooFew and tooMany for too few and too many arguments made first.

cfamily.CheckDialect.convertValues

def CheckDialect.convertValues {L : Constructs} (d : CheckDialect L) (g : Globals L) (n : NodeId) (name : String) (ps : List (Ty L)) (es : List (TypedExpr L)) : CheckResult L (List (TypedExpr L))

The arguments es converted to the parameters’ types ps where nothing can run first (a library function’s parameters are C’s types), by the dialect d for the program’s tables g; a wrong count is refused at the call’s node n with the function’s name.

cfamily.CheckDialect.defaults

def CheckDialect.defaults {L : Constructs} (n : NodeId) (missing : Refusal) (ds : List (Defaulted L)) : CheckResult L (LiftedList L)

The arguments for defaulted parameters (all must have defaults): their statements and values; a parameter without one is refused as missing says.

cfamily.Defaulted.trailing

def Defaulted.trailing {L : Constructs} (ds : List (Defaulted L)) : Nat

How many of the last parameters have defaults (ds, one for each parameter).

cfamily.CheckDialect.resultOf

def CheckDialect.resultOf {L : Constructs} (d : CheckDialect L) (n : NodeId) (t : Ty L) : TypedExpr L

The expression a call’s result is: the dialect’s for its types, else the temporary named for the node.

cfamily.CheckDialect.printArguments

def CheckDialect.printArguments {L : Constructs} (d : CheckDialect L) (n : NodeId) (es : List (TypedExpr L)) : CheckResult L (List (TypedExpr L))

The arguments of printf and sprintf after the default argument promotions (C11 6.5.2.2p6): integers promoted, floating values as double; strings as pointers; other pointers are not supported.

cfamily.CheckDialect.promotedFloat

def CheckDialect.promotedFloat {L : Constructs} (d : CheckDialect L) (t : Ty L) : FloatFormat

The format a floating argument of the type t has after the default argument promotions: long double’s when it is long double, else double’s.

cfamily.CheckDialect.printArgument

def CheckDialect.printArgument {L : Constructs} (d : CheckDialect L) (n : NodeId) (e : TypedExpr L) : CheckResult L (TypedExpr L)

One argument of printf after the default argument promotions (C11 6.5.2.2p6): float becomes double, long double stays.

cfamily.CheckDialect.scanTargets

def CheckDialect.scanTargets {L : Constructs} (d : CheckDialect L) (n : NodeId) (es : List (TypedExpr L)) : CheckResult L (List (TypedExpr L))

The targets of scanf and sscanf: pointers to integers or floating objects.

cfamily.CheckDialect.callConverted

def CheckDialect.callConverted {L : Constructs} (d : CheckDialect L) (g : Globals L) (n : NodeId) (f : String) (result : Ty L) (args : LiftedList L) (es : List (TypedExpr L)) (statement : Option (DeclId * Ty L) -> List (TypedExpr L) -> TypedStmt L) : CheckResult L (Lifted L)

A call with checked arguments already converted: the call into a temporary named for the node (the result’s type, declared in the caller’s scope), and the callee’s effects as accesses.

cfamily.CheckDialect.variadicArguments

def CheckDialect.variadicArguments {L : Constructs} (d : CheckDialect L) (g : Globals L) (n : NodeId) (lf : LibraryFunction L) (es : List (TypedExpr L)) : CheckResult L (List (TypedExpr L))

The arguments of a library function that takes more after its parameters: the parameters’ converted, the rest as printf’s arguments or scanf’s targets.

cfamily.CheckDialect.wantsLongDoubleMath

def CheckDialect.wantsLongDoubleMath {L : Constructs} (d : CheckDialect L) (es : List (TypedExpr L)) : Bool

Whether a math function’s arguments es call for an overload the model does not have: where the rules overload the functions by type (C++’s ), an argument of long double’s format other than double’s (the long double overload computes in it; converting to double would give double’s result).

cfamily.CheckDialect.libraryArguments

def CheckDialect.libraryArguments {L : Constructs} (d : CheckDialect L) (g : Globals L) (n : NodeId) (lf : LibraryFunction L) (es : List (TypedExpr L)) : CheckResult L (List (TypedExpr L))

The arguments es of the library function lf called at the node n (in the dialect d with the globals g) converted: to its parameters’ types, and any after them as it takes them. A math function given a long double where the rules overload it by type is not decided (CheckDialect.wantsLongDoubleMath).

cfamily.CheckDialect.sizeArgument

def CheckDialect.sizeArgument {L : Constructs} (d : CheckDialect L) (n : NodeId) (e : TypedExpr L) : CheckResult L (TypedExpr L)

A size argument as size_t.

cfamily.CheckDialect.allocationSize

def CheckDialect.allocationSize {L : Constructs} (d : CheckDialect L) (n : NodeId) (f : String) (es : List (TypedExpr L)) : CheckResult L (TypedExpr L)

The bytes malloc (one argument) or calloc (two, multiplied) allocates.

cfamily.CheckDialect.reallocated

def CheckDialect.reallocated {L : Constructs} (d : CheckDialect L) (n : NodeId) (element : Ty L) (old : TypedExpr L) : CheckResult L (TypedExpr L)

realloc’s first argument: a pointer to the element type, or a null pointer constant (realloc(NULL, n) is malloc).

cfamily.CheckDialect.reallocation

def CheckDialect.reallocation {L : Constructs} (d : CheckDialect L) (n : NodeId) (t : Ty L) (element : Ty L) (elementSize : Nat) (args : LiftedList L) : CheckResult L (Lifted L)

realloc(old, size) into a pointer to the element: the pointer in a temporary named for the node.

cfamily.CheckDialect.allocation

def CheckDialect.allocation {L : Constructs} (d : CheckDialect L) (g : Globals L) (n : NodeId) (f : String) (t : Ty L) (args : LiftedList L) : CheckResult L (Lifted L)

malloc, calloc or realloc into a pointer of the expected type: size bytes (calloc zeroes them) of the pointed-to complete object type, the pointer in a temporary named for the node.

cfamily.CheckDialect.isAllocation

def CheckDialect.isAllocation {L : Constructs} (g : Globals L) (f : String) : Bool

Whether a call by name is malloc, calloc or realloc of the library (the program does not define the name).

cfamily.CheckDialect.address

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

&lvalue: a pointer to the lvalue’s type, const kept.

cfamily.CheckDialect.indirectValue

def CheckDialect.indirectValue {L : Constructs} (d : CheckDialect L) (g : Globals L) (n : NodeId) (x : Lifted L) : CheckResult L (Lifted L)

*a as a value: *fp is the function again (it decays back to the pointer), else the lvalue read. An lvalue of a type known only by name has no value to read: it is kept as the lvalue (a reference binds to it, & takes its address), and what would read it needs the type complete (a declaration, sizeof, a member, an assignment, a parameter or result by value: C11 6.3.2.1p2, C++17 [conv.lval]p1).

cfamily.CheckDialect.discardedIndirection

def CheckDialect.discardedIndirection {L : Constructs} (d : CheckDialect L) (g : Globals L) (n : NodeId) (x : Lifted L) : Option (CheckResult L (Statements L))

A discarded *p (an expression statement, a cast to void, the left of a comma) with p a pointer to an object type: where the rules read a discarded lvalue (C11 6.3.2.1p2), the read is undefined for a type known only by name, rejected, and any other p is checked as a value (none); else (C++17 [expr]p12: no lvalue-to-rvalue conversion) nothing is read, but the indirection is still made: its result is the object p points to ([expr.unary.op]p1), so a null pointer, one to an object whose lifetime ended or one past the end stops the run as reading through it would. None for any other operand (a function pointer, a class with operator: checked as a value, as before). The dialect d, the globals g (to complete the pointed-to type), the node n of the *, and the checked operand x.

cfamily.CheckDialect.functionName

def CheckDialect.functionName {L : Constructs} (g : Globals L) (n : NodeId) (f : String) : CheckResult L (Lifted L)

A function’s name as a value: a pointer to it (C11 6.3.2.1p4).

cfamily.CheckDialect.temporary

def CheckDialect.temporary {L : Constructs} (d : CheckDialect L) (n : NodeId) (x : Lifted L) : Lifted L

A value that is not an lvalue kept in a temporary named for the node.

cfamily.CheckDialect.undeclaredCall

def CheckDialect.undeclaredCall {L : Constructs} (n : NodeId) (f : String) : CheckResult L (Lifted L)

A call by a name nothing declares: malloc without a pointer type to take, or an undeclared function.

cfamily.TypedStmt.libraryCalling

def TypedStmt.libraryCalling {L : Constructs} (n : NodeId) (f : String) (target : Option (DeclId * Ty L)) (es : List (TypedExpr L)) : TypedStmt L

The call statement of a library function.

cfamily.TypedStmt.calling

def TypedStmt.calling {L : Constructs} (n : NodeId) (f : String) (target : Option (DeclId * Ty L)) (es : List (TypedExpr L)) : TypedStmt L

The call statement of a function of the program.

cfamily.CheckDialect.matched

def CheckDialect.matched {L : Constructs} (d : CheckDialect L) (g : Globals L) (n : NodeId) (sg : Signature L) (xs : LiftedList L) : CheckResult L (LiftedList L)

A call’s arguments for a function’s parameters: the missing ones from their defaults, all converted.

cfamily.CheckDialect.matching

def CheckDialect.matching {L : Constructs} (d : CheckDialect L) (g : Globals L) (n : NodeId) (sg : Signature L) (xs : LiftedList L) : CheckResult L (LiftedList L)

A call’s arguments matched to a function’s parameters (CheckDialect.matched), a mismatch rejected or not provided as the dialect reports it.

cfamily.CheckDialect.missingDefaults

def CheckDialect.missingDefaults {L : Constructs} (n : NodeId) (sg : Signature L) (given : Nat) : CheckResult L (LiftedList L)

The arguments of the missing parameters, from their defaults (none if all are given).

cfamily.LiftedList.followedBy

def LiftedList.followedBy {L : Constructs} (a : LiftedList L) (b : LiftedList L) : LiftedList L

Expressions followed by more, in order.

cfamily.CheckDialect.pointerCall

def CheckDialect.pointerCall {L : Constructs} (d : CheckDialect L) (n : NodeId) (c : Lifted L) (xs : LiftedList L) (pointer : TypedExpr L) (t : Ty L) (es : List (TypedExpr L)) : Lifted L

A call through the pointer with converted arguments, into a temporary; any effects.

cfamily.Checker.fuel

def Checker.fuel : Nat

The fuel for checking one expression: deeper nesting than this is rejected.

cfamily.Expr.check

def Expr.check {L : Constructs} (d : CheckDialect L) (g : Globals L) (env : Env L) (e : Expr) : CheckResult L (Lifted L)

Checks an expression in a scope.

cfamily.Expr.checkLvalue

def Expr.checkLvalue {L : Constructs} (d : CheckDialect L) (g : Globals L) (env : Env L) (e : Expr) : CheckResult L (Lifted L)

Checks an expression used as an lvalue (not read).

cfamily.Expr.checkAgainst

def Expr.checkAgainst {L : Constructs} (d : CheckDialect L) (g : Globals L) (env : Env L) (t : Ty L) (e : Expr) : CheckResult L (Lifted L)

Checks an expression against an expected type (malloc’s result takes its type from it).

cfamily.Checker.of

def Checker.of {L : Constructs} (d : CheckDialect L) : Checker L

The core’s checker, for a dialect’s code outside expressions (statements).