cogent/examples/system-abstract-verif/main.ac

// Prototypes of our abstract functions are inserted into Kernel.c above
// Now we define our two abstract functions
$ty:(U64) memMagicNumber($ty:(KernelState!) arg) {
    return arg->magicNumber;
}

$ty:(()) kernelPanic($ty:(KernelState) arg) {
#ifndef KERNEL_VERIFICATION
    fprintf(arg->kernelLogStream, "%s\n", KERNEL_PANIC_MESSAGE);
#endif // KERNEL_VERIFICATION

    free(arg);
    exit(1);

    struct unit_t u;
    return u;
}

// Our main function, to test
int main(void)
{
    $ty:(KernelState) state = malloc(sizeof (KernelState));
    state->magicNumber = 0xdeadbeef;
    state->kernelLogStream = stdout;

    $ty:(Result KernelState) res = kernelStatusCheck(state);
    if (res.tag == TAG_ENUM_Error) {
        // We should have kernel panicked by now
    } else {
        // Collect the state back from the function
        state = res.Success;
    }

    // Only call this function if we are not verifying - autocorres doesn't like the string literal
    // we need to format the print
#ifndef KERNEL_VERIFICATION
    fprintf(state->kernelLogStream, "%s\n", KERNEL_OK_MESSAGE);
#endif // KERNEL_VERIFICATION

    free(state);

    return 0;
}