clibrary

cfamily.VariadicArguments

data VariadicArguments

What a library function takes after its parameters: nothing, arguments as printf’s (sprintf), or targets as scanf’s (sscanf).

cfamily.LibraryFunction

record LibraryFunction (L : Constructs)

A library function: name, parameter types, result type (none is void), the effects of a call, the parameters it writes through when they are the only ones (a call whose arguments there are all null pointer constants writes nothing: strtol with no end pointer), and what it takes after its parameters.

cfamily.LibraryFunction.reading

def LibraryFunction.reading : Effects

What reading through its arguments’ pointers does: reads elsewhere.

cfamily.LibraryFunction.writing

def LibraryFunction.writing : Effects

What writing through its arguments’ pointers does: writes and reads elsewhere.

cfamily.LibraryFunction.reads

def LibraryFunction.reads : Effects

What reading input into its arguments’ pointers does.

cfamily.LibraryFunction.prints

def LibraryFunction.prints : Effects

What printing to the console does (%s reads through a pointer).

cfamily.LibraryFunction.of

def LibraryFunction.of {L : Constructs} (name : String) (parameters : List (Ty L)) (result : Ty L) (effects : Effects) : LibraryFunction L

A library function returning a value.

cfamily.LibraryFunction.writingThrough

def LibraryFunction.writingThrough {L : Constructs} (name : String) (parameters : List (Ty L)) (result : Ty L) (indices : List Nat) : LibraryFunction L

A library function returning a value that writes only through the parameters at the indices.

cfamily.LibraryFunction.variadic

def LibraryFunction.variadic {L : Constructs} (name : String) (parameters : List (Ty L)) (result : Ty L) (rest : VariadicArguments) : LibraryFunction L

A library function returning int that takes more arguments after its parameters.

cfamily.LibraryFunction.variadicWritingThrough

def LibraryFunction.variadicWritingThrough {L : Constructs} (name : String) (parameters : List (Ty L)) (result : Ty L) (rest : VariadicArguments) (indices : List Nat) : LibraryFunction L

The library function name returning result that takes more arguments after its parameters (as rest says) and writes only through the parameters at the indices (sprintf’s buffer).

cfamily.LibraryTypes

record LibraryTypes (L : Constructs)

The types the library’s signatures use, on a target.

cfamily.LibraryTypes.of

def LibraryTypes.of {L : Constructs} (tgt : Target) : LibraryTypes L

The signatures’ types on a target: size_t as the platform’s ABI has it, FILE is opaque, wchar_t is int.

cfamily.LibraryFunction.input

def LibraryFunction.input {L : Constructs} (t : LibraryTypes L) : List (LibraryFunction L)

<stdio.h>’s functions: the console, the files, formatted input and output.

cfamily.LibraryFunction.strings

def LibraryFunction.strings {L : Constructs} (t : LibraryTypes L) : List (LibraryFunction L)

<string.h>’s functions.

cfamily.LibraryFunction.characters

def LibraryFunction.characters {L : Constructs} (t : LibraryTypes L) : List (LibraryFunction L)

<ctype.h>’s functions.

cfamily.LibraryFunction.mathematics

def LibraryFunction.mathematics {L : Constructs} (t : LibraryTypes L) : List (LibraryFunction L)

<math.h>’s functions.

cfamily.LibraryFunction.utilities

def LibraryFunction.utilities {L : Constructs} (t : LibraryTypes L) : List (LibraryFunction L)

<stdlib.h>’s functions (malloc, calloc, realloc and free are checked by their own rules).

cfamily.LibraryFunction.randomAndTime

def LibraryFunction.randomAndTime {L : Constructs} (tgt : Target) (t : LibraryTypes L) : List (LibraryFunction L)

<stdlib.h>’s random numbers and <time.h>’s clock (time_t is long): checked by their own rules when called.

cfamily.LibraryFunction.wide

def LibraryFunction.wide {L : Constructs} (t : LibraryTypes L) : List (LibraryFunction L)

<wchar.h>’s functions (wchar_t is int).

cfamily.LibraryFunction.sortChecks

def LibraryFunction.sortChecks {L : Constructs} (t : LibraryTypes L) : List (LibraryFunction L)

The checks qsort and bsearch make.

cfamily.LibraryFunction.standard

def LibraryFunction.standard {L : Constructs} (tgt : Target) : List (LibraryFunction L)

The C library functions on a target.

cfamily.LibraryFunction.isMath

def LibraryFunction.isMath (tgt : Target) (f : String) : Bool

Whether f names one of <math.h>’s functions (LibraryFunction.mathematics), on the target tgt.

cfamily.LibraryFunction.named

def LibraryFunction.named {L : Constructs} (fs : List (LibraryFunction L)) (f : String) : Option (LibraryFunction L)

The library function with the name, if any.

cfamily.LibraryFunction.writesThroughOf

def LibraryFunction.writesThroughOf {L : Constructs} (fs : List (LibraryFunction L)) (f : String) : List Nat

The arguments (by position) the function named f of the library fs writes through when those are all it writes elsewhere (snprintf’s buffer, memcpy’s destination); none for a function the library does not have.

cfamily.LibraryConstant

record LibraryConstant

A macro constant of the standard headers (C11 5.2.4.2.1 <limits.h>, 7.21.1 <stdio.h>’s EOF, 7.22 <stdlib.h>’s RAND_MAX and EXIT_*): its name, the headers that declare it (C’s and C++’s spelling), its type and its value on a platform. A program writes it as eConst.

cfamily.LibraryConstant.promoted

def LibraryConstant.promoted (p : Platform) (t : IntegerType) : IntegerType

The type a limit of t has: t after the integer promotions (C11 5.2.4.2.1p1: UCHAR_MAX is an int).

cfamily.LibraryConstant.maximumIn

def LibraryConstant.maximumIn (headers : List String) (name : String) (t : Platform -> IntegerType) : LibraryConstant

The largest value of a type, as a limit some headers declare.

cfamily.LibraryConstant.minimumIn

def LibraryConstant.minimumIn (headers : List String) (name : String) (t : Platform -> IntegerType) : LibraryConstant

The smallest value of a type, as a limit some headers declare.

cfamily.LibraryConstant.maximumOf

def LibraryConstant.maximumOf (name : String) (t : Platform -> IntegerType) : LibraryConstant

The largest value of a type, as a limit of <limits.h>.

cfamily.LibraryConstant.minimumOf

def LibraryConstant.minimumOf (name : String) (t : Platform -> IntegerType) : LibraryConstant

The smallest value of a type, as a limit of <limits.h>.

cfamily.LibraryConstant.fixed

def LibraryConstant.fixed (name : String) (headers : List String) (v : Int) : LibraryConstant

An int constant a header declares, the same on every platform.

cfamily.LibraryConstant.standard

def LibraryConstant.standard : List LibraryConstant

The macro constants of the standard headers. RAND_MAX is INT_MAX on the platforms modeled (glibc, Apple’s libc, AVR libc and newlib all define it so; the standard only asks for at least 32767). C++’s std::string::npos (size_type(-1), [basic.string]) is here too, written with or without std::: only C++ names have ::.

cfamily.LibraryConstant.limitsOf

def LibraryConstant.limitsOf (start : String) (signed : Platform -> IntegerType) (unsigned : Platform -> IntegerType) : List LibraryConstant

The limits of <stdint.h> for one of its types: INTN_MIN, INTN_MAX, UINTN_MAX and so on (C11 7.20.2).

cfamily.LibraryConstant.integerLimits

def LibraryConstant.integerLimits : List LibraryConstant

The limits of <stdint.h> (C11 7.20.2, 7.20.3): each one’s type is its type’s after the integer promotions.

cfamily.LibraryConstant.named

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

The macro constant of that name, if a standard header declares one.

cfamily.LibraryConstant.included

def LibraryConstant.included {L : Constructs} (g : Globals L) (c : LibraryConstant) : Bool

Whether the program includes one of the headers that declare a constant.

cfamily.LibraryFunction.allocation

def LibraryFunction.allocation : List String

The allocation functions: the checker models them by its own rules rather than a signature.

cfamily.LibraryFunction.specialEffects

def LibraryFunction.specialEffects : List (String * Effects)

The effects of the library functions checked by their own rules rather than a signature: allocation, variadic formatting, the random numbers and the clock.

cfamily.LibraryFunction.isNull

def LibraryFunction.isNull {L : Constructs} (e : Option (TypedExpr L)) : Bool

Whether an argument is there and a null pointer constant.

cfamily.LibraryFunction.effectsWith

def LibraryFunction.effectsWith {L : Constructs} (f : LibraryFunction L) (args : List (TypedExpr L)) : Effects

The effects of a call with its arguments: none of the writes when every argument it writes through is a null pointer constant.

cfamily.LibraryFunction.effectsOf

def LibraryFunction.effectsOf {L : Constructs} (fs : List (LibraryFunction L)) (f : String) (args : List (TypedExpr L)) : Effects

The effects of calling a function by name that the program does not define: the library’s, or (for a function the library does not have) reading elsewhere.