Library mcertikos.devdrivers.ConsoleBuffIntroGenLinkSource
*********************************************************************** * * * The CertiKOS Certified Kit Operating System * * * * The FLINT Group, Yale University * * * * Copyright The FLINT Group, Yale University. All rights reserved. * * This file is distributed under the terms of the Yale University * * Non-Commercial License Agreement. * * * ***********************************************************************
Require Import LinkSourceTemplate.
Require Import MBoot.
Require Import MBootCSource.
Require Import CDataTypes.
Definition DConsoleBuffIntro_module: link_module :=
{|
lm_cfun :=
lcf cons_buf_init f_cons_buf_init ::
lcf cons_buf_write f_cons_buf_write ::
lcf cons_buf_read f_cons_buf_read ::
lcf cons_buf_wpos f_cons_buf_wpos ::
nil;
lm_asmfun :=
nil;
lm_gvar :=
lgv cons_buf_LOC cons_buf_loc_type ::
nil
|}.
Definition DConsoleBuffIntro_impl `{CompCertiKOS} `{RealParams} :=
link_impl DConsoleBuffIntro_module mboot.