integer

cfamily.Rank

data Rank

The integer conversion rank (C11 6.3.1.1p1): bool < char < short < int < long < long long.

cfamily.Rank.order

def Rank.order (r : Rank) : Nat

The order of a rank, from 0 for bool.

cfamily.Rank.belowNormal

def Rank.belowNormal (r : Rank) : Bool

Whether a rank is below int’s: such types are promoted.

cfamily.Rank.width

def Rank.width (p : Platform) (r : Rank) : Nat

The width of a rank’s type on a platform (bool’s is 1).

cfamily.IntegerType

record IntegerType

An integer type: signedness, rank, width in bits, and whether it is plain char.

cfamily.Platform

record Platform

A platform’s integer and pointer widths, whether plain char is signed, and the greatest alignment a scalar has in bytes (a scalar is aligned to its size up to it).

cfamily.Platform.aligned

def Platform.aligned (p : Platform) (bytes : Nat) : Nat

The alignment of a scalar of a size in bytes on a platform.

cfamily.Platform.lp64

def Platform.lp64 : Platform

LP64, the usual desktop and server platform (Linux and macOS; char signed as on x86-64).

cfamily.Platform.avr

def Platform.avr : Platform

AVR, the Arduino Uno’s platform: 16-bit int and pointers, 32-bit long; every type aligned to 1 byte (avr-gcc’s ABI: no padding).

cfamily.Platform.esp

def Platform.esp : Platform

ESP32 and ESP8266 (the Xtensa and RISC-V GCC): 32-bit int, long and pointers, plain char unsigned.

cfamily.IntegerType.boolean

def IntegerType.boolean : IntegerType

bool.

cfamily.IntegerType.signedChar

def IntegerType.signedChar : IntegerType

signed char.

cfamily.IntegerType.unsignedChar

def IntegerType.unsignedChar : IntegerType

unsigned char.

cfamily.IntegerType.char

def IntegerType.char (p : Platform) : IntegerType

Plain char: signed or not as the platform says.

cfamily.IntegerType.short

def IntegerType.short (p : Platform) : IntegerType

short.

cfamily.IntegerType.unsignedShort

def IntegerType.unsignedShort (p : Platform) : IntegerType

unsigned short.

cfamily.IntegerType.int

def IntegerType.int (p : Platform) : IntegerType

int.

cfamily.IntegerType.unsignedInt

def IntegerType.unsignedInt (p : Platform) : IntegerType

unsigned int.

cfamily.IntegerType.long

def IntegerType.long (p : Platform) : IntegerType

long.

cfamily.IntegerType.unsignedLong

def IntegerType.unsignedLong (p : Platform) : IntegerType

unsigned long.

cfamily.IntegerType.longLong

def IntegerType.longLong (p : Platform) : IntegerType

long long.

cfamily.IntegerType.unsignedLongLong

def IntegerType.unsignedLongLong (p : Platform) : IntegerType

unsigned long long.

cfamily.IntegerType.sameType

def IntegerType.sameType (a : IntegerType) (b : IntegerType) : Bool

Whether two types are the same type (plain char differs from both signed and unsigned char).

cfamily.IntegerType.minimum

def IntegerType.minimum (t : IntegerType) : Int

The least value of a type.

cfamily.IntegerType.maximum

def IntegerType.maximum (t : IntegerType) : Int

The greatest value of a type.

cfamily.IntegerType.inRange

def IntegerType.inRange (t : IntegerType) (v : Int) : Bool

Whether a value is in a type’s range.

cfamily.IntegerType.covers

def IntegerType.covers (u : IntegerType) (t : IntegerType) : Bool

Whether u can represent every value of t; compares widths and signedness only, so no 2^width is built.

cfamily.IntegerType.promote

def IntegerType.promote (p : Platform) (t : IntegerType) : IntegerType

The integer promotions: a type ranked below int, or a bit-field narrower than its type that fits in int’s width, becomes int if int covers it, else unsigned int (C11 6.3.1.1p2).

cfamily.IntegerType.unsignedVersion

def IntegerType.unsignedVersion (t : IntegerType) : IntegerType

The unsigned type of the same rank and width.

cfamily.IntegerType.firstOfWidth

def IntegerType.firstOfWidth (w : Nat) (ts : List IntegerType) : Option IntegerType

The first of some types that is w bits wide, if any.

cfamily.IntegerType.difference

def IntegerType.difference (p : Platform) : IntegerType

ptrdiff_t and intptr_t: the first of int, long and long long as wide as a pointer (long on LP64’s glibc, int in AVR libc and in the ESP chips’ newlib).

cfamily.IntegerType.size

def IntegerType.size (p : Platform) : IntegerType

size_t and uintptr_t: the unsigned type of ptrdiff_t’s rank.

cfamily.IntegerType.maximal

def IntegerType.maximal (p : Platform) : IntegerType

intmax_t: long when it is as wide as long long (glibc), else long long.

cfamily.IntegerType.unsignedMaximal

def IntegerType.unsignedMaximal (p : Platform) : IntegerType

uintmax_t: the unsigned type of intmax_t’s rank.

cfamily.IntegerType.exactly

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

intN_t (and int_leastN_t): the first of signed char, int, short, long and long long that is w bits wide (short for 16 bits and long for 64 on LP64’s glibc; int for 16 bits and long for 32 in AVR libc).

cfamily.IntegerType.commonMixed

def IntegerType.commonMixed (s : IntegerType) (u : IntegerType) : IntegerType

The common type of a signed and an unsigned promoted type.

cfamily.IntegerType.commonPromoted

def IntegerType.commonPromoted (a : IntegerType) (b : IntegerType) : IntegerType

The common type of two promoted types: the higher rank if their signedness agrees, else by commonMixed.

cfamily.IntegerType.common

def IntegerType.common (p : Platform) (a : IntegerType) (b : IntegerType) : IntegerType

The usual arithmetic conversions on two integer types: promote both, then take the common type.

cfamily.IntegerType.convert

def IntegerType.convert (t : IntegerType) (v : Int) : Int

Any integer converted to the type: whether it is nonzero for bool, else modulo 2^width (two’s complement if signed).