@cella-lang/c

C11 for the Cella proof checker, as a compiled module pack: the C branch of the C family's deep embedding (@cella-lang/cfamily). A program is checked by C11's rules and run by a small-step semantics; the verdict is accept, reject or unknown, with the node and the clause of the standard.

Depends on @cella-lang/cfamily and @cella-lang/machine.

Programs

The JSON of cfamily's syntax with "lang": {"k": "langC"}, on LP64. The branch covers the integer types with C's promotions and conversions, control flow (if, loops, switch, goto), arrays (multi-dimensional, variable length, const), pointers with their provenance, malloc, realloc and free, structs and unions, function pointers, floating point and <math.h>, <string.h> and <ctype.h>, printf, scanf and their string and file forms, strtok, qsort and bsearch, and standard input. A C program names no board (one that does is invalid: an Arduino program is C++).

Entries

• c.verdict src input fuel: the verdict JSON (format in @cella-lang/cfamily); input is standard input, fuel bounds the steps. A verdict proved by the kernels: kernel_verdict_in("c", "c.verdict", …) in cella-lang.
• c.types src candidates: the type query (format in @cella-lang/cfamily).
• The debugger, for cella-lang/dap: load, run, stopConf, stopKind, stopNode, stopOut, stopErr, stopDetail, divergences, feed, globals, frames, setVarErr, setVarConf, env; and report input fuel session, a whole run with all the input given at once.

Loading

Load the packs into the cella-lang build named by index.json (checkerHash, cbfVersion; the peerDependencies pin it): the standard modules in index.requires["cella-lang"].modules, the packages in index.requires.packages (each the same way), then this package's modules in the order of index.modules.c.deps. cella-lang's README (Official packages) has the code.

Per-definition hashes

index.json lists, for every definition, own (its own content) and merkle (its content and everything it depends on). A definition whose merkle did not change between two versions means the same; a changed one is listed in CHANGES.md.