Library mcertikos.devdrivers.HandlerOpGenLinkSource
*********************************************************************** * * * 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 DHandlerCxt.
Require Import DHandlerCxtCSource.
Require Import CDataTypes.
Section HandlerOpGenLinkSource.
Definition DHandlerOp_module : link_module :=
{|
lm_cfun :=
lcf serial_intr_disable_handler f_serial_intr_disable_handler ::
lcf serial_intr_enable_handler f_serial_intr_enable_handler ::
nil;
lm_asmfun :=
nil;
lm_gvar :=
nil
|}.
Definition DHandlerOp_impl `{CompCertiKOS} `{RealParams} :=
link_impl DHandlerOp_module dhandlercxt.
End HandlerOpGenLinkSource.