standardlibrary

cfamily.LibraryDialect

record LibraryDialect (L : Constructs)

What running the library needs: the target, the type extension and the program’s tables (element sizes), and how new objects are made (memset of zero).

cfamily.Returned

record Returned (L : Constructs)

What a function returns (none for void), and the state after it.

cfamily.Returned.with

def Returned.with {L : Constructs} (s : State L) (v : Value) : Evaluated L (Returned L)

Returning a value.

cfamily.Returned.integer

def Returned.integer {L : Constructs} (s : State L) (v : Int) : Evaluated L (Returned L)

Returning an integer.

cfamily.Returned.count

def Returned.count {L : Constructs} {A : Type} (s : State L) (xs : List A) : Evaluated L (Returned L)

Returning a count.

cfamily.Object.integer

def Object.integer (v : Int) : Object

An initialized integer object.

cfamily.State.print

def State.print {L : Constructs} (s : State L) (text : String) : State L

The state with text written to the standard output.

cfamily.State.consume

def State.consume {L : Constructs} (s : State L) (rest : List Char) : State L

The state with the input consumed to rest.

cfamily.Library.notNull

def Library.notNull (c : Nat) : Bool

Whether a code is not the null.

cfamily.State.objectsFrom

def State.objectsFrom {L : Constructs} (s : State L) (p : Pointer) : Option (List Object)

The objects a pointer ranges over from where it points: the elements after it (or the object, taken as an array of one).

cfamily.State.room

def State.room {L : Constructs} (s : State L) (p : Pointer) : Nat

How many elements are left from where a pointer points (0 for any pointer that is not into a live block).

cfamily.Pointer.literalCodes

def Pointer.literalCodes (text : String) (i : Int) : List Nat

The bytes of a string literal from an index, up to its end.

cfamily.Object.stringBytes

def Object.stringBytes {L : Constructs} (n : NodeId) (os : List Object) : Evaluated L (List Nat)

The bytes of objects up to a null, read as unsigned char (C11 7.1.1p1): an uninitialized one is indeterminate, no null before the end is out of bounds.

cfamily.State.string

def State.string {L : Constructs} (n : NodeId) (s : State L) (p : Pointer) : Evaluated L (List Nat)

The string a pointer points to, without its null.

cfamily.Object.boundedBytes

def Object.boundedBytes {L : Constructs} (n : NodeId) (limit : Nat) (os : List Object) : Evaluated L (List Nat)

At most limit bytes of objects, up to a null (strncpy’s and strncat’s source): an uninitialized one is indeterminate, the objects ending first is out of bounds.

cfamily.State.boundedString

def State.boundedString {L : Constructs} (n : NodeId) (s : State L) (p : Pointer) (limit : Nat) : Evaluated L (List Nat)

At most limit bytes of the string a pointer points to, without its null.

cfamily.Object.exactBytes

def Object.exactBytes {L : Constructs} (n : NodeId) (count : Nat) (os : List Object) : Evaluated L (List Nat)

Exactly count bytes of objects (memchr and memcmp read them all, nulls included).

cfamily.State.viewedBytes

def State.viewedBytes {L : Constructs} (n : NodeId) (s : State L) (p : Pointer) (count : Nat) : Evaluated L (List Nat)

Exactly count bytes of an object’s from where a pointer to its bytes points.

cfamily.State.exactBytes

def State.exactBytes {L : Constructs} (d : LibraryDialect L) (n : NodeId) (s : State L) (p : Pointer) (count : Nat) : Evaluated L (List Nat)

Exactly count bytes from where a pointer points: a string literal’s include its null; an object that is not of a character type has bytes the model does not know (C11 6.2.6.1p1).

cfamily.Object.bytesUpTo

def Object.bytesUpTo (limit : Option Nat) (os : List Object) : Option (List Nat)

At most limit bytes of objects (or up to a null): none if one is uninitialized, or the objects end first.

cfamily.State.reader

def State.reader {L : Constructs} (s : State L) (p : Pointer) (limit : Option Nat) : Option (List Nat)

printf’s %s reader for a pointer: the bytes up to a null or the precision, none where reading is undefined.

cfamily.Pointer.elementAddress

def Pointer.elementAddress (p : Pointer) (k : Nat) : Address

The address of the k-th element after where a pointer points.

cfamily.Pointer.offset

def Pointer.offset (p : Pointer) (j : Int) : Pointer

The pointer j elements on (the caller has checked the range).

cfamily.State.writeAt

def State.writeAt {L : Constructs} (s : State L) (a : Address) (o : Object) : State L

The state with an object written at an address (nothing changes where it cannot be written).

cfamily.State.writeObjects

def State.writeObjects {L : Constructs} (s : State L) (p : Pointer) (j : Nat) (os : List Object) : State L

Objects written from the j-th element after a pointer on.

cfamily.State.writeBytes

def State.writeBytes {L : Constructs} (s : State L) (p : Pointer) (t : IntegerType) (k : Nat) (bytes : List Nat) : State L

Bytes written as values of a character type from the k-th element on, then a null.

cfamily.State.writeCharacters

def State.writeCharacters {L : Constructs} (s : State L) (p : Pointer) (t : IntegerType) (bytes : List Nat) : State L

The bytes written through p in the state s as values of the character type t, from the first element on, with no null after them (scanf’s %c).

cfamily.Pointer.writable

def Pointer.writable (p : Pointer) : Option Behavior

Why a pointer cannot be written through by the library: null, a string literal, a stream.

cfamily.State.writable

def State.writable {L : Constructs} (rules : Rules) (s : State L) (p : Pointer) : Option Behavior

Why a pointer cannot be written through by the library: as Pointer.writable, or an object defined const (C11 6.7.3p6).

cfamily.State.elementType

def State.elementType {L : Constructs} (d : LibraryDialect L) (s : State L) (p : Pointer) : Ty L

The type of the elements a pointer ranges over.

cfamily.LibraryDialect.size

def LibraryDialect.size {L : Constructs} (d : LibraryDialect L) (t : Ty L) : Nat

The size of a type on the target.

cfamily.Pointer.overlaps

def Pointer.overlaps (p : Pointer) (lp : Nat) (q : Pointer) (lq : Nat) : Bool

Whether two ranges of elements overlap (in the same array).

cfamily.Library.argument

def Library.argument (vs : List Value) (k : Nat) : Value

The value of the k-th argument (0 if there are too few: the checker gives every function its count).

cfamily.Library.integer

def Library.integer (vs : List Value) (k : Nat) : Int

The int value of an argument.

cfamily.Library.pointer

def Library.pointer (vs : List Value) (k : Nat) : Pointer

The pointer value of an argument.

cfamily.Library.text

def Library.text (codes : List Nat) : String

The text of codes.

cfamily.Library.putchar

def Library.putchar {L : Constructs} (s : State L) (c : Int) : Evaluated L (Returned L)

putchar: writes c converted to unsigned char and returns it.

cfamily.Library.puts

def Library.puts {L : Constructs} (n : NodeId) (s : State L) (p : Pointer) : Evaluated L (Returned L)

puts: the string and a newline (a pointer that is not to a string is undefined); returns 0.

cfamily.Library.getchar

def Library.getchar {L : Constructs} (s : State L) : Evaluated L (Returned L)

getchar: the next byte, or EOF (-1) at the end of the input.

cfamily.Library.line

def Library.line (cs : List Char) (m : Nat) : List Char

A line of at most m characters (the newline included).

cfamily.Library.fgets

def Library.fgets {L : Constructs} (d : LibraryDialect L) (n : NodeId) (s : State L) (buffer : Pointer) (count : Int) (stream : Pointer) : Evaluated L (Returned L)

fgets: at most n - 1 characters of a stream up to a newline, then a null; NULL when nothing is read at the end.

cfamily.Library.fopen

def Library.fopen {L : Constructs} (n : NodeId) (s : State L) (name : Pointer) (written : Pointer) : Evaluated L (Returned L)

fopen: a stream for the file, or NULL when a file to read does not exist.

cfamily.Library.fgetc

def Library.fgetc {L : Constructs} (n : NodeId) (s : State L) (stream : Pointer) : Evaluated L (Returned L)

fgetc: the next byte of a stream as unsigned char, or EOF at the end.

cfamily.Library.fputc

def Library.fputc {L : Constructs} (n : NodeId) (s : State L) (c : Int) (stream : Pointer) : Evaluated L (Returned L)

fputc: a byte (the character as unsigned char) to a stream; returns it.

cfamily.Library.files

def Library.files {L : Constructs} (n : NodeId) (s : State L) (f : String) (vs : List Value) : Evaluated L (Returned L)

The file functions: fopen, fclose, fputs, fputc, putc, fgetc, getc, feof.

cfamily.Library.fileNames

def Library.fileNames : List String

The file functions’ names.

cfamily.Library.compare

def Library.compare (a : List Nat) (b : List Nat) : Int

strcmp’s result: the difference of the first differing bytes (as clang’s libc; the standard fixes only the sign).

cfamily.Library.copy

def Library.copy {L : Constructs} (d : LibraryDialect L) (n : NodeId) (s : State L) (destination : Pointer) (offset : Nat) (source : Pointer) (bytes : List Nat) : Evaluated L (Returned L)

strcpy (offset 0) and strcat (offset the destination’s length): room for the bytes and the null, no overlap with the source (C11 7.24.2.3p2).

cfamily.ParsedNumber

record ParsedNumber

A number as strtol reads it: whether negative, the magnitude, how many digits, how many bytes used (0 with no digits: the end points at the start).

cfamily.Library.digit

def Library.digit (c : Nat) : Nat

The value of a digit up to base 36 (99 if none).

cfamily.Library.readDigits

def Library.readDigits (base : Nat) (cs : List Nat) (acc : Nat) (count : Nat) : Nat * Nat

Digits of a base: the value and how many.

cfamily.Library.hexStart

def Library.hexStart (cs : List Nat) : Bool

Whether the codes start with 0x and a hexadecimal digit.

cfamily.Library.parseNumber

def Library.parseNumber (base : Nat) (cs : List Nat) : ParsedNumber

strtol’s reading (C11 7.22.1.4): white space, a sign, a prefix by the base (0x for 16 and 0, 0 is octal for 0), digits.

cfamily.ParsedNumber.value

def ParsedNumber.value (r : ParsedNumber) : Int

The value read.

cfamily.Library.atoi

def Library.atoi {L : Constructs} (d : LibraryDialect L) (n : NodeId) (s : State L) (bytes : List Nat) : Evaluated L (Returned L)

atoi: as strtol in base 10, but a value out of int’s range is undefined (C11 7.22.1p1).

cfamily.Library.strtol

def Library.strtol {L : Constructs} (d : LibraryDialect L) (n : NodeId) (s : State L) (text : Pointer) (bytes : List Nat) (finish : Pointer) (base : Int) : Evaluated L (Returned L)

strtol: the base is 0 or 2 to 36; a value out of long’s range is LONG_MAX or LONG_MIN (ERANGE, not undefined); the end is written through end unless it is NULL.

cfamily.Library.between

def Library.between (lo : Nat) (hi : Nat) (v : Int) : Bool

Whether v is in [lo, hi].

cfamily.Library.ctype

def Library.ctype (f : String) (v : Int) : Int

A <ctype.h> function of a character code.

cfamily.Library.ctypeNames

def Library.ctypeNames : List String

The <ctype.h> functions.

cfamily.Library.repeatByte

def Library.repeatByte (b : Nat) (k : Nat) : Nat

An integer’s bytes repeated (memset of an element of k bytes).

cfamily.Library.fill

def Library.fill {L : Constructs} (m : Making L) (e : Ty L) (byte : Nat) : Option Object

The object memset fills an element with: an integer element the byte repeated; any other element only zero.

cfamily.Library.elements

def Library.elements {L : Constructs} (d : LibraryDialect L) (e : Ty L) (bytes : Int) : Option Nat

The count of whole elements in a length of bytes, if the length is a positive multiple of the element size.

cfamily.Library.memset

def Library.memset {L : Constructs} (d : LibraryDialect L) (n : NodeId) (s : State L) (p : Pointer) (c : Int) (bytes : Int) : Evaluated L (Returned L)

memset: the destination’s elements filled (C11 7.24.6.1).

cfamily.State.sourceObjects

def State.sourceObjects {L : Constructs} (s : State L) (p : Pointer) : List Object

The objects a source pointer gives (a string literal’s bytes, its null included).

cfamily.Object.asByte

def Object.asByte {L : Constructs} (t : Ty L) (o : Object) : Object

A character object as a byte of another character type: its value converted (an initialized byte’s bits kept, two’s complement).

cfamily.Library.memcpy

def Library.memcpy {L : Constructs} (d : LibraryDialect L) (n : NodeId) (s : State L) (move : Bool) (given : Pointer) (origin : Pointer) (bytes : Int) : Evaluated L (Returned L)

memcpy and memmove: the same element type on both sides (or character types, byte by byte: objects of other types as their bytes, Pointer.asBytes), whole elements, room on both; memcpy’s ranges must not overlap (C11 7.24.2.1p2).

cfamily.Library.math

def Library.math (f : FloatFormat) (name : String) (x : Float) (y : Float) : Float

The <math.h> functions on double: round halfway away from zero (C11 7.12.9.6) and trunc toward zero, on the exact value; fmod exactly; the others correctly rounded.

cfamily.Library.mathNames

def Library.mathNames : List String

The <math.h> functions.

cfamily.Library.inexactMathNames

def Library.inexactMathNames : List String

The <math.h> functions whose accuracy the C standard leaves to the implementation (C11 5.2.4.2.2p6): the model gives the correctly rounded result, which the verdict assumes of the platform’s math library (libm:math.correctlyRounded; glibc and Apple’s libm are within an ulp but not always correctly rounded). sqrt is exact by IEEE 754, fmod exact.

cfamily.Library.mathematics

def Library.mathematics {L : Constructs} (d : LibraryDialect L) (n : NodeId) (s : State L) (f : String) (x : Float) (y : Float) : Evaluated L (Returned L)

A <math.h> function’s result, with the assumption on the math library when the standard leaves its accuracy open.

cfamily.Library.infinityNames

def Library.infinityNames : List String

What <math.h>’s INFINITY and HUGE_VAL expand to: positive infinity (C11 7.12p4, p3; IEEE 754 has infinities).

cfamily.Library.abs

def Library.abs {L : Constructs} (d : LibraryDialect L) (n : NodeId) (s : State L) (t : IntegerType) (v : Int) : Evaluated L (Returned L)

abs: -INT_MIN does not fit (C11 7.22.6.1p2).

cfamily.Library.checkArray

def Library.checkArray {L : Constructs} (d : LibraryDialect L) (n : NodeId) (s : State L) (base : Pointer) (count : Int) (size : Int) : Evaluated L (Returned L)

qsort’s and bsearch’s array (C11 7.22.5p1): a valid pointer even for 0 elements (not NULL, to a live object); for more, size the element’s and all n elements in the array.

cfamily.Library.sign

def Library.sign (v : Int) : Int

A comparison’s sign: -1, 0 or 1.

cfamily.Library.checkOrder

def Library.checkOrder {L : Constructs} (n : NodeId) (s : State L) (c : Int) (r : Int) (z : Bool) : Evaluated L (Returned L)

qsort’s check of two elements of the sorted array, i before j (C11 7.22.5p4): c compares the i-th with the j-th, r the j-th with the i-th, and z says whether every neighbour from the i-th to the j-th compares equal. The results agree with an order the array is sorted by when c is not above 0, r has the opposite sign, and c is 0 exactly when z says so (the equal elements are the runs of equal neighbours).

cfamily.Library.checkSorted

def Library.checkSorted {L : Constructs} (n : NodeId) (s : State L) (a : Int) (b : Int) : Evaluated L (Returned L)

bsearch’s check of two neighbouring elements (C11 7.22.5.1p2): a compares the key with the one before, b with the one after; the elements below the key come first, then the equal ones, then the ones above.

cfamily.Library.hold

def Library.hold {L : Constructs} (s : State L) (base : Pointer) (count : Int) : State L

qsort’s and bsearch’s array held while they run (C11 7.22.5p3: the comparator is not to alter it): the elements from the base on, or the whole object a pointer to one points to; a pointer into the bytes of an object is not held (the check misses writes there, it does not reject).

cfamily.Library.release

def Library.release {L : Constructs} (s : State L) : State L

The innermost held array let go.

cfamily.Library.swap

def Library.swap {L : Constructs} (s : State L) (p : Pointer) (i : Nat) (j : Nat) : State L

The i-th and j-th elements swapped (whole objects).

cfamily.Library.printArgument

def Library.printArgument {L : Constructs} (p : Platform) (s : State L) (e : TypedExpr L) (v : Value) : PrintArgument

printf’s argument for the value v of the expression e (on the platform p, reading strings in s): a pointer is a string (read when the conversion needs it), a floating value a long double when its type’s precision is above binary64’s (x87’s extended format) and a double otherwise, an integer of the expression’s type.

cfamily.Library.printArguments

def Library.printArguments {L : Constructs} (p : Platform) (s : State L) (es : List (TypedExpr L)) (vs : List Value) : List PrintArgument

The arguments of a formatted output.

cfamily.Library.printf

def Library.printf {L : Constructs} (p : Platform) (n : NodeId) (s : State L) (format : String) (es : List (TypedExpr L)) (vs : List Value) : Evaluated L (State L)

printf: the formatted output on the console (a mismatch is undefined, C11 7.21.6.1p9).

cfamily.Library.printfCounted

def Library.printfCounted {L : Constructs} (p : Platform) (n : NodeId) (s : State L) (format : String) (es : List (TypedExpr L)) (vs : List Value) : Evaluated L (Returned L)

printf of format on the platform p at the node n, as a call whose value is used: the output of the arguments es (their values vs) on the console of s, and the count of bytes written (C11 7.21.6.3p3).

cfamily.Library.sprintf

def Library.sprintf {L : Constructs} (d : LibraryDialect L) (n : NodeId) (s : State L) (destination : Pointer) (format : List Nat) (es : List (TypedExpr L)) (vs : List Value) : Evaluated L (Returned L)

sprintf: the output and its null written to the destination (no room is out of bounds); returns its length.

cfamily.Library.snprintf

def Library.snprintf {L : Constructs} (d : LibraryDialect L) (n : NodeId) (s : State L) (destination : Pointer) (size : Nat) (format : List Nat) (es : List (TypedExpr L)) (vs : List Value) : Evaluated L (Returned L)

snprintf: at most size - 1 bytes of the output, then a null (nothing for size 0, the buffer may then be NULL); the result is the whole output’s length (C11 7.21.6.5).

cfamily.Library.fprintf

def Library.fprintf {L : Constructs} (d : LibraryDialect L) (n : NodeId) (s : State L) (stream : Pointer) (format : List Nat) (es : List (TypedExpr L)) (vs : List Value) : Evaluated L (Returned L)

fprintf: the output to a stream; the result is its length.

cfamily.ScanPlace

record ScanPlace (L : Constructs)

A scanf argument: the pointer, its object’s type, and what scanf may read into it (a character array takes bytes with room for what is left of it).

cfamily.Library.place

def Library.place {L : Constructs} (d : LibraryDialect L) (n : NodeId) (s : State L) (e : TypedExpr L) (v : Value) : Evaluated L (ScanPlace L)

The place an argument of pointer type points to (a string literal cannot be written, C11 6.4.5p7).

cfamily.Library.places

def Library.places {L : Constructs} (d : LibraryDialect L) (n : NodeId) (s : State L) (es : List (TypedExpr L)) (vs : List Value) : Evaluated L (List (ScanPlace L))

The places of scanf’s arguments, in order.

cfamily.Library.writeScanned

def Library.writeScanned {L : Constructs} (s : State L) (places : List (ScanPlace L)) (values : List Scanned) : State L

The values scanf read written to their places (bytes with a null after them).

cfamily.Library.scanInto

def Library.scanInto {L : Constructs} (d : LibraryDialect L) (n : NodeId) (s : State L) (format : String) (input : List Nat) (es : List (TypedExpr L)) (vs : List Value) : Evaluated L (ScanResult * State L)

Scanning an input into the arguments’ places: the count, and the state with the values written.

cfamily.Library.scanf

def Library.scanf {L : Constructs} (d : LibraryDialect L) (n : NodeId) (s : State L) (format : String) (es : List (TypedExpr L)) (vs : List Value) : Evaluated L (Returned L)

scanf on the console’s input: the values written, the input consumed.

cfamily.Library.fscanf

def Library.fscanf {L : Constructs} (d : LibraryDialect L) (n : NodeId) (s : State L) (stream : Pointer) (format : List Nat) (es : List (TypedExpr L)) (vs : List Value) : Evaluated L (Returned L)

fscanf: scanning a stream’s input; what was read is consumed.

cfamily.Library.sscanf

def Library.sscanf {L : Constructs} (d : LibraryDialect L) (n : NodeId) (s : State L) (input : List Nat) (format : List Nat) (es : List (TypedExpr L)) (vs : List Value) : Evaluated L (Returned L)

sscanf: scanning a string (stdin is not touched).

cfamily.Library.copyBounded

def Library.copyBounded {L : Constructs} (d : LibraryDialect L) (n : NodeId) (s : State L) (destination : Pointer) (source : Pointer) (count : Nat) (bytes : List Nat) : Evaluated L (Returned L)

strncpy: the source’s bytes up to count, then nulls up to count (no null when the source is that long): room for count, no overlap (C11 7.24.2.4).

cfamily.Library.among

def Library.among (set : List Nat) (b : Nat) : Bool

Whether a byte is one of a set’s.

cfamily.Library.span

def Library.span (inside : Bool) (set : List Nat) (bytes : List Nat) : List Nat

The leading bytes that are in the set (inside true) or not in it (inside false).

cfamily.Library.firstAmong

def Library.firstAmong (set : List Nat) (k : Nat) (bytes : List Nat) : Option Nat

The index of the first byte in the set, if any.

cfamily.Library.breakAt

def Library.breakAt {L : Constructs} (s : State L) (p : Pointer) (set : List Nat) (bytes : List Nat) : Evaluated L (Returned L)

strpbrk: a pointer to the first byte in the set, or NULL.

cfamily.Library.memchr

def Library.memchr {L : Constructs} (d : LibraryDialect L) (n : NodeId) (s : State L) (p : Pointer) (c : Int) (count : Int) : Evaluated L (Returned L)

memchr: the first of count bytes equal to the character (as unsigned char), or NULL.

cfamily.Library.memcmp

def Library.memcmp {L : Constructs} (d : LibraryDialect L) (n : NodeId) (s : State L) (p : Pointer) (q : Pointer) (count : Int) : Evaluated L (Returned L)

memcmp: count bytes of each, compared as unsigned char.

cfamily.Object.wideValues

def Object.wideValues {L : Constructs} (n : NodeId) (os : List Object) : Evaluated L (List Int)

The values of objects up to a null (wide characters: not converted to bytes): an uninitialized one is indeterminate, no null before the end is out of bounds.

cfamily.State.wideString

def State.wideString {L : Constructs} (n : NodeId) (s : State L) (p : Pointer) : Evaluated L (List Int)

The wide string a pointer points to, without its null.

cfamily.Library.compareWide

def Library.compareWide (a : List Int) (b : List Int) : Int

The sign of the first difference of two wide strings (wcscmp).

cfamily.Library.copyWide

def Library.copyWide {L : Constructs} (d : LibraryDialect L) (n : NodeId) (s : State L) (destination : Pointer) (offset : Nat) (source : Pointer) (values : List Int) : Evaluated L (Returned L)

wcscpy (offset 0) and wcscat (offset the destination’s length): room for the values and the null, no overlap.

cfamily.Library.wide

def Library.wide {L : Constructs} (d : LibraryDialect L) (n : NodeId) (s : State L) (f : String) (vs : List Value) : Evaluated L (Returned L)

The wide string functions: wcslen, wcscmp, wcscpy, wcscat.

cfamily.Library.wideNames

def Library.wideNames : List String

The wide string functions’ names.

cfamily.Library.tokenFrom

def Library.tokenFrom {L : Constructs} (d : LibraryDialect L) (n : NodeId) (s : State L) (start : Pointer) (delimiters : List Nat) : Evaluated L (Returned L)

strtok from where it starts: the delimiters before the token skipped; the delimiter after it, if any, made a null (the string must be writable) and the next call goes on after it; NULL once no token is left (C11 7.24.5.8).

cfamily.Library.strtok

def Library.strtok {L : Constructs} (d : LibraryDialect L) (n : NodeId) (s : State L) (p : Pointer) (delimiters : List Nat) : Evaluated L (Returned L)

strtok: a string starts over, NULL goes on from where the last call ended (undefined before any call).

cfamily.Library.terminated

def Library.terminated (bytes : List Nat) : List Nat

A string’s bytes with its terminating null (strchr and strrchr find the null too).

cfamily.Library.charOf

def Library.charOf (vs : List Value) : Nat

The character a call’s second argument gives, converted to char and read as the byte it is stored as.

cfamily.Library.firstAt

def Library.firstAt (k : Nat) (c : Nat) (bytes : List Nat) : Option Nat

Where a byte first is among bytes, from k.

cfamily.Library.lastAt

def Library.lastAt (k : Nat) (c : Nat) (found : Option Nat) (bytes : List Nat) : Option Nat

Where a byte last is among bytes, from k (found: the last one so far).

cfamily.Library.prefixOf

def Library.prefixOf (start : List Nat) (bytes : List Nat) : Bool

Whether bytes begin with the bytes of start.

cfamily.Library.substringAt

def Library.substringAt (k : Nat) (needle : List Nat) (bytes : List Nat) : Option Nat

Where a needle first starts in bytes, from k (an empty needle at once).

cfamily.Library.located

def Library.located {L : Constructs} (s : State L) (p : Pointer) (at : Option Nat) : Evaluated L (Returned L)

A pointer k past p where something was found, or NULL.

cfamily.Library.charAt

def Library.charAt (last : Bool) (c : Nat) (bytes : List Nat) : Option Nat

strchr (the first) or strrchr (the last): where the character is in a string’s bytes, its null included.

cfamily.Library.atol

def Library.atol {L : Constructs} (d : LibraryDialect L) (n : NodeId) (s : State L) (bytes : List Nat) : Evaluated L (Returned L)

atol: like atoi, in long’s range (a value it cannot hold is undefined, C11 7.22.1.2).

cfamily.Library.atof

def Library.atof {L : Constructs} (d : LibraryDialect L) (n : NodeId) (s : State L) (bytes : List Nat) : Evaluated L (Returned L)

atof: strtod(s, NULL) after the white space (C11 7.22.1.1); no number is 0, a value it cannot represent is undefined.

cfamily.Library.withStrings

def Library.withStrings {L : Constructs} (n : NodeId) (s : State L) (p : Pointer) (q : Pointer) (next : List Nat -> List Nat -> Evaluated L (Returned L)) : Evaluated L (Returned L)

The bytes of the strings two arguments point to, then what to do with them.

cfamily.Library.strings

def Library.strings {L : Constructs} (d : LibraryDialect L) (n : NodeId) (s : State L) (f : String) (vs : List Value) : Evaluated L (Returned L)

The string functions: strlen, strcmp, strcpy, strcat, atoi, strtol.

cfamily.Library.stringNames

def Library.stringNames : List String

The string functions’ names.

cfamily.Library.isIn

def Library.isIn (names : List String) (f : String) : Bool

Whether a name is in a list.

cfamily.Library.memory

def Library.memory {L : Constructs} (d : LibraryDialect L) (n : NodeId) (s : State L) (f : String) (vs : List Value) : Evaluated L (Returned L)

The memory functions and the checks of qsort and bsearch.

cfamily.Library.memoryNames

def Library.memoryNames : List String

The memory functions’ names.

cfamily.Library.isCharacterOrEof

def Library.isCharacterOrEof (v : Int) : Bool

A character code, or EOF, that <ctype.h> accepts (C11 7.4p1).

cfamily.Library.formatted

def Library.formatted {L : Constructs} (d : LibraryDialect L) (n : NodeId) (s : State L) (f : String) (es : List (TypedExpr L)) (vs : List Value) : Evaluated L (Returned L)

printf, scanf, sprintf, snprintf, fprintf, fscanf and sscanf: the format (and sscanf’s input) are strings.

cfamily.Library.wordSize

def Library.wordSize : Nat

2^32: glibc’s random number words are unsigned 32-bit.

cfamily.Library.randomStep

def Library.randomStep (words : List Nat) : List Nat * Nat

The next word of glibc’s random number generator (TYPE_3, an additive feedback generator): from the 34 most recent r[i-34] … r[i-1], r[i] = r[i-31] + r[i-3] modulo 2^32; the words move on by one.

cfamily.Library.randomAdvance

def Library.randomAdvance (k : Nat) (words : List Nat) : List Nat

The generator moved on by k words.

cfamily.Library.randomSeedWords

def Library.randomSeedWords (k : Nat) (previous : Int) : List Int

glibc’s seeding of r[1] … r[30] from r[0]: r[i] = 16807 * r[i-1] % 2147483647, as C’s remainder (with the sign of the dividend), made non-negative.

cfamily.Library.randomWord

def Library.randomWord (v : Int) : Nat

A word as glibc stores it: the 32-bit two’s complement of an int.

cfamily.Library.randomSeeded

def Library.randomSeeded (seed : Int) : List Nat

The generator after srand(seed) (glibc’s srandom_r, TYPE_3): r[0] is the seed as an int (1 for 0), r[1] … r[30] from it, r[31] … r[33] repeat r[0] … r[2], and the 310 words after are dropped.

cfamily.Library.rand

def Library.rand {L : Constructs} (n : NodeId) (s : State L) : Evaluated L (Returned L)

rand() (C11 7.22.2.1): the sequence is the implementation’s; this is glibc’s (r[i] >> 1), seeded with 1 before any srand. The verdict assumes it (rand.sequence, noted on the state as the library’s choices are).

cfamily.Library.srand

def Library.srand {L : Constructs} (n : NodeId) (s : State L) (seed : Int) : Evaluated L (Returned L)

srand(seed): glibc’s generator seeded (C11 7.22.2.2).

cfamily.Library.time

def Library.time {L : Constructs} (n : NodeId) (s : State L) (p : Pointer) : Evaluated L (Returned L)

time(p) (C11 7.27.2.4): the calendar time is the environment’s; the model reads 0, written through p unless it is null. The verdict assumes it (time.now).

cfamily.Library.call

def Library.call {L : Constructs} (d : LibraryDialect L) (n : NodeId) (s : State L) (f : String) (es : List (TypedExpr L)) (vs : List Value) : Evaluated L (Returned L)

A library function by name on its arguments (the expressions give the arguments’ types for the formatted ones).