Integer arithmetic on an unknown stays folded when a premise is computed (Symbolic.v).

The symbols laying out hello_module gives, from 65536 on (initial_memory): 115 of them, functions and data.

A genv links Hello: its module is hello_module, each of the module's symbols is where hello_globals puts it, and no libc function the module calls (hello_externals) is a symbol, so each such call is an external_site. Startup may add libc's data symbols, such as program_invocation_name.

The module md defines no function named s (find_fn).

A function md does not define is no function of a genv with module md: find_fn reads only the module.

The libc function s, one Hello calls, is no function of a genv with Hello's module.

The function f called with the words xs, at its entry, as call_frame makes it; a direct call to f binds this frame.

Block l of f, or an empty one.

mbszero(p): memset of 8 zero bytes, gnulib's mbstate_t reset.

memeq(p, q, n): memcmp, compared with 0.

streq(p, q): strcmp, compared with 0.

strnlen1(p, n): memchr for the NUL in n bytes; one past it, or n.

xmalloc(n): malloc, and xalloc_die on null.

mbszero's one block.

memeq's one block.

streq's one block.

strnlen1's entry: memchr, then is its result null?

strnlen1 after a hit: one past it.

strnlen1 after no hit: n.

xmalloc's entry: malloc, then is the result null?

xmalloc's return.

mbszero has its block.

memeq has its block.

streq has its block.

strnlen1 has its entry.

strnlen1 has its hit block.

strnlen1 has its miss block.

xmalloc has its entry.

xmalloc has its return block.

mbszero's entry binds its pointer.

memeq's entry binds its pointers and length.

streq's entry binds its pointers.

strnlen1's entry binds its pointer and bound.

xmalloc's entry binds its size.

Prove a premise that names words: by computation, with the environment's facts.

Prove an address premise: drop the wraps of raw_address and of a flight's sum where arithmetic shows them the identity, then arithmetic.

Hello's leaf functions over any runtimeruntime Fil-CThe runtime is what Fil-C does around one thread's program, natively libpizlo.so with FUGC: where a new object goes, what free does, and what the collector may change while the program waits at a safepoint. The model does not define it; it states it as one page of axioms, Module Type Runtime (Runtime), each with a native test in tests/c/prog/axiom-*.c. R.