lengths

cfamily.ConstantValue

data ConstantValue

What an expression is as a constant expression: a constant of an integer type, a constant of a floating type (its format and value), not a constant expression by the dialect’s rules, or something the model does not decide (why).

cfamily.ConstantScope

record ConstantScope

What evaluating constant expressions needs: the dialect’s rules and target, the constants known so far (by their declarations’ labels), the declarations whose constancy the model does not decide, and the typedefs.

cfamily.ConstantScope.of

def ConstantScope.of (rules : Rules) (target : Target) (constants : List (DeclId * Int)) (typedefs : List (String * TypeSyntax)) : ConstantScope

The scope of the dialect’s rules and target with the constants known (by their declarations’ labels) and the typedefs, none undecided: the one a case label or an enumerator’s value is read in.

cfamily.ConstantScope.bytes

def ConstantScope.bytes (width : Nat) : Nat

The bytes of a width in bits (at least one: bool is one byte).

cfamily.ConstantScope.expanded

def ConstantScope.expanded (s : ConstantScope) (fuel : Nat) (t : TypeSyntax) : TypeSyntax

The written type t with its typedef names (from s) replaced, at its top (fuel bounds the chains).

cfamily.ConstantScope.integerTypeWithin

def ConstantScope.integerTypeWithin (s : ConstantScope) (fuel : Nat) (t : TypeSyntax) : Option IntegerType

The integer type the written type t is (through the typedefs of s, without its const), if it is one; fuel bounds the const layers peeled.

cfamily.ConstantScope.integerType

def ConstantScope.integerType (s : ConstantScope) (t : TypeSyntax) : Option IntegerType

The integer type the written type t is (through the typedefs of s, without its const), if it is one.

cfamily.ConstantScope.sizeOf

def ConstantScope.sizeOf (s : ConstantScope) (fuel : Nat) (t : TypeSyntax) : Option Nat

The size in bytes of the written type t when it does not need a layout (C11 6.5.3.4): integer, floating and pointer types, arrays of them, through the typedefs of s (on the target of s); none for a struct, union or class (their layout comes later). fuel bounds the typedef chains.

cfamily.ConstantScope.namedType

def ConstantScope.namedType (s : ConstantScope) (v : Int) : IntegerType

The type of a constant variable’s or enumeration constant’s value v: int (on the target of s) when it holds v, else long long.

cfamily.ConstantScope.truthType

def ConstantScope.truthType (s : ConstantScope) : IntegerType

The type of a truth value: int in C, bool in C++ (as the rules of s type true).

cfamily.ConstantScope.truth

def ConstantScope.truth (s : ConstantScope) (b : Bool) : ConstantValue

The truth value b as a constant of the truth type of s.

cfamily.ConstantScope.undefinedWhy

def ConstantScope.undefinedWhy : String

Why a constant expression’s value is not decided: an operation whose result is undefined (a signed overflow, a division by zero, a shift out of range) makes an expression that is not a constant expression (C11 6.6p4, C++ [expr.const]p2.6), which the model does not judge.

cfamily.ConstantScope.result

def ConstantScope.result (t : IntegerType) (v : Int) : ConstantValue

The arithmetic result v in its type t: a signed one out of range is undefined, an unsigned one wraps.

cfamily.ConstantScope.quotientFits

def ConstantScope.quotientFits (t : IntegerType) (a : Int) (b : Int) : Bool

Whether the quotient of a by b is a value of the type t: always for an unsigned type (it wraps), in range for a signed one.

cfamily.ConstantScope.divide

def ConstantScope.divide (t : IntegerType) (remainder : Bool) (a : Int) (b : Int) : ConstantValue

a / b (or a % b when remainder) in the type t: b not zero, a signed quotient in range (C11 6.5.5p5-6).

cfamily.ConstantScope.fitsUnsigned

def ConstantScope.fitsUnsigned (t : IntegerType) (v : Int) : Bool

Whether the value v is below 2 to the width of the type t: a value of the unsigned type of that width.

cfamily.ConstantScope.shift

def ConstantScope.shift (s : ConstantScope) (t : IntegerType) (left : Bool) (a : Int) (b : Int) : ConstantValue

a << b (when left) or a >> b in the promoted left type t: 0 <= b < width; a signed left shift of a negative value is undefined, and of a value too large is undefined in C, the unsigned counterpart’s value in C++17 (as the rules of s say; C11 6.5.7p3-4, [expr.shift]p2).

cfamily.ConstantValue.both

def ConstantValue.both (a : ConstantValue) (b : ConstantValue) (f : IntegerType -> Int -> IntegerType -> Int -> ConstantValue) : ConstantValue

f applied to both operands’ types and values (a’s, then b’s), or the first operand that is not a constant.

cfamily.ConstantScope.call

def ConstantScope.call (s : ConstantScope) : ConstantValue

A call in a constant expression: none in C; in C++ maybe a constexpr function, which the model does not know (the rules of s say which).

cfamily.ConstantScope.floatTruth

def ConstantScope.floatTruth (s : ConstantScope) (b : Bool) : ConstantValue

A truth value b computed from floating operands: in C++ a constant of the truth type of s; in C not an integer constant expression (a floating operand is only the immediate operand of a cast, C11 6.6p6).

cfamily.ConstantScope.isTrueFloat

def ConstantScope.isTrueFloat (x : Float) : Bool

Whether the floating value x counts as true (it is not zero; NaN is true), as a condition does.

cfamily.ConstantScope.floatResult

def ConstantScope.floatResult (f : FloatFormat) (x : Float) : ConstantValue

The floating result x in the format f: a constant when finite; an infinity or NaN (an overflow, a division by zero) is undefined, so not a constant expression (C11 6.6p4, C++ [expr.pre]p4 and [expr.const]p2.6).

cfamily.ConstantValue.commonFormat

def ConstantValue.commonFormat (a : ConstantValue) (b : ConstantValue) : Option FloatFormat

The format of the usual arithmetic conversions of the constants a and b when one is floating (the wider one’s, C11 6.3.1.8p1); none when neither is.

cfamily.ConstantValue.asFloat

def ConstantValue.asFloat (f : FloatFormat) (a : ConstantValue) : Option Float

The constant a as a value of the floating format f (an integer converted, C11 6.3.1.4p2; a floating one rounded to f), if it is a constant.

cfamily.ConstantScope.truncated

def ConstantScope.truncated (t : IntegerType) (x : Float) : ConstantValue

The floating constant x converted to the integer type t (C11 6.3.1.4p1, C++ [conv.fpint]p1): to bool its truth; otherwise truncated toward zero, which must be a value of t (else the behavior is undefined: not a constant expression, C11 6.6p4, C++ [expr.const]p2.6).

cfamily.ConstantScope.converted

def ConstantScope.converted (s : ConstantScope) (t : IntegerType) (immediate : Bool) (a : ConstantValue) : ConstantValue

The constant a converted to the integer type t (as an initializer or a cast does), in the scope s: an integer is converted (C11 6.3.1.3); a floating value is truncated where the rules let it into an integer constant expression, or when immediate (the operand is a floating constant itself, C11 6.6p6); otherwise not a constant expression.

cfamily.ConstantScope.unary

def ConstantScope.unary (s : ConstantScope) (n : NodeId) (op : UnaryOp) (a : ConstantValue) : ConstantValue

The unary operator op (at the node n) on the constant a in the scope s (after the integer promotions; ! gives a truth value; ~ of a floating value is not one).

cfamily.ConstantScope.isTrue

def ConstantScope.isTrue (v : Int) : Bool

Whether the scalar value v counts as true (it is not zero), as an operand of && and || does.

cfamily.ConstantScope.floatBinary

def ConstantScope.floatBinary (s : ConstantScope) (op : BinaryOp) (f : FloatFormat) (x : Float) (y : Float) : ConstantValue

The binary operator op on the floating values x and y of the format f in the scope s: the arithmetic correctly rounded (machine.float), the comparisons and && and || truth values (ConstantScope.floatTruth); the others do not take floating operands.

cfamily.ConstantValue.bothFloat

def ConstantValue.bothFloat (f : FloatFormat) (a : ConstantValue) (b : ConstantValue) (k : Float -> Float -> ConstantValue) : ConstantValue

The constants a and b as values of the floating format f, given to k; the first that is not a constant otherwise.

cfamily.ConstantScope.integerBinary

def ConstantScope.integerBinary (s : ConstantScope) (n : NodeId) (op : BinaryOp) (a : ConstantValue) (b : ConstantValue) : ConstantValue

The binary operator op (at the node n) on the integer constants a and b in the scope s: && and || and the comparisons give truth values; a shift has the left operand’s promoted type; the others the usual arithmetic conversions (C11 6.5, C++ [expr]).

cfamily.ConstantScope.binary

def ConstantScope.binary (s : ConstantScope) (n : NodeId) (op : BinaryOp) (a : ConstantValue) (b : ConstantValue) : ConstantValue

The binary operator op (at the node n) on the constants a and b in the scope s: on floating values when either is one (ConstantScope.floatBinary, after the usual arithmetic conversions), else on integers (ConstantScope.integerBinary).

cfamily.ConstantScope.truthOf

def ConstantScope.truthOf (s : ConstantScope) (c : ConstantValue) : Option Bool

Whether the constant c is true as a condition, in the scope s (a floating one where the rules let floating values into integer constant expressions); none when it is not such a constant.

cfamily.ConstantValue.failedCondition

def ConstantValue.failedCondition (c : ConstantValue) : ConstantValue

What a condition c that is not a true or false constant makes of the expression: a floating one (in C) is not a constant expression; otherwise c itself.

cfamily.ConstantScope.conditional

def ConstantScope.conditional (s : ConstantScope) (c : ConstantValue) (a : ConstantValue) (b : ConstantValue) : ConstantValue

c ? a : b on constants in the scope s: both arms constant (C11 6.6p6), the chosen one in their common type (floating when either is).

cfamily.ConstantScope.floatFormat

def ConstantScope.floatFormat (s : ConstantScope) (t : TypeSyntax) : Option FloatFormat

The floating format of the written type t (read through the typedefs of s), if it is double or float.

cfamily.ConstantScope.cast

def ConstantScope.cast (s : ConstantScope) (t : TypeSyntax) (immediate : Bool) (a : ConstantValue) : ConstantValue

A cast of the constant a to the written type t (read through the typedefs of s): an integer type converts it (ConstantScope.converted; immediate when the operand is a floating constant itself); a floating type rounds it to its format; any other type is not an integer constant expression.

cfamily.Expr.isFloatingConstant

def Expr.isFloatingConstant (e : Expr) : Bool

Whether the expression e is a floating constant as written (without a sign, which makes an expression: C11 6.4.4.2), the operand C11 6.6p6 lets a cast to an integer type convert.

cfamily.ConstantScope.value

def ConstantScope.value (s : ConstantScope) (e : Expr) : ConstantValue

The value of the expression e as a constant expression by the dialect’s rules, with the constants known in s (C11 6.6p6; C++17 [expr.const]): see the module’s table.

cfamily.ConstantSource

data ConstantSource

A source of constants, in the program’s order: enumerators (each without a value the previous one’s plus one) and a variable with its written type and initializer.

cfamily.ConstantScope.withEnumerators

def ConstantScope.withEnumerators (s : ConstantScope) (next : Option Int) (cs : List Enumerator) : ConstantScope

The scope s with the enumeration’s constants cs: next is the value of one without a written value (none once one’s value is not decided, C11 6.7.2.2p3).

cfamily.ConstantScope.with

def ConstantScope.with (s : ConstantScope) (source : ConstantSource) : ConstantScope

The scope with a source’s constants: a variable counts where the rules make const integral variables constants, when its type is a const integer type and its initializer a constant expression (its value converted to the type, a floating one truncated, ConstantScope.converted); one whose initializer the model does not decide is undecided too.

cfamily.ConstantSource.ofStatement

def ConstantSource.ofStatement (st : Stmt) : List ConstantSource

The constants the statement st declares (a variable with an initializer expression, an enumeration in a block).

cfamily.ConstantSource.ofFunction

def ConstantSource.ofFunction (f : FunctionDefinition) : List ConstantSource

The constants in the body of the function f, in order.

cfamily.ConstantSource.ofClass

def ConstantSource.ofClass (d : ClassDefinition) : List ConstantSource

The constants of the class definition d.

cfamily.ArrayLengths.typedefs

def ArrayLengths.typedefs (items : List Item) : List (String * TypeSyntax)

The typedefs among the file-scope items (a block’s are moved there later; a length that names one is then not decided).

cfamily.ArrayLengths.constants

def ArrayLengths.constants (rules : Rules) (target : Target) (items : List Item) : ConstantScope

The scope of constants of a program’s items, for a dialect’s rules and target.

cfamily.ArrayLengths.lowerType

def ArrayLengths.lowerType (s : ConstantScope) (t : TypeSyntax) : TypeSyntax

The written type t, when an array whose length is a constant greater than zero in the scope s, as tArr (others as they are).

cfamily.ArrayLengths.problem

def ArrayLengths.problem {L : Constructs} (s : ConstantScope) (t : TypeSyntax) : Option (CheckResult L (List Item))

What the length of the written type t, left after lowering, means in the scope s: a constant zero or below or of a floating type is rejected, an undecided one is unknown; one that is not a constant is left to the checker (none).

cfamily.ArrayLengths.firstProblem

def ArrayLengths.firstProblem {L : Constructs} (s : ConstantScope) (ts : List TypeSyntax) : Option (CheckResult L (List Item))

The first problem among the written types ts, in the scope s.

cfamily.ArrayLengths.lowered

def ArrayLengths.lowered {L : Constructs} (rules : Rules) (target : Target) (items : List Item) : CheckResult L (List Item)

The items with every array whose length is written as an expression decided by the dialect’s rules on the target (see the module’s description): a positive constant length made tArr; a constant zero or below rejected; an undecided one unknown; the others left.