Enough of an executable semantics to execute a not-quite-trivial program, plus a patch for compcert to convert C to a matita definition.