Library mcertikos.devdrivers.HandlerOpGenLinkSource

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} `{MultiOracleProp} `{WaitTime} :=
    link_impl DHandlerOp_module dhandlercxt.

End HandlerOpGenLinkSource.