The VSU for external axiomatized functions is much like any other VSU, except that we use Axioms instead of Definitions and Lemmas. Because this VSU does not import any APDs, we don't need a Section. Normally at this point, we would construct an M showing how the mem_mgr predicate is implemented. But here we just axiomatize:

Normally at this point, we would prove a semax_body lemma for each function that the module exports. But here, we use body_lemma_of_funspec for external functions; and we write this as an axiom:

Internal functions

There is one internal (nonexported) function, so as usual we must write a funspec for it. That is, the placeholder, which is a useless function whose only purpose was to force clightgen to keep the external declarations for malloc, free, exit. Because nobody will call placeholder(), we can give it a trivial funspec whose precondition is False.

Definining the pieces of a VSU

And now, in the usual way, we can put totether the pieces:

Constructing the Component and the VSU

This lemma is required for the solve_SF_external (body_malloc) below. The basic purpose is to ensure that the postcondition of the external function ensures a return value that's strictly compatible with the calling conventions specified by the C-language return-type of the function. The particular form of the lemma is derived from the proof goal of solve_SF_external below.

Each VSU may have private global variables that constitute its "local state". This VSU_initializer lemma calculates how to reason about their initial values. But the module stdlib.c does not have any global variables, so this initialize lemma is rather trivial here. See VSU_stdlib2.v, lemma initialize, for a more interesting example.

Now that all the subcomponents are ready, we can bundle up the VSU:

Next Chapter: VSU_main