Library mcertikos.devdrivers.HandlerGenLinkSource

Require Import LinkSourceTemplate.
Require Import DHandlerOp.
Require Import DHandlerOpCSource.
Require Import CDataTypes.

Section HandlerGenLinkSource.

  Definition DHandler_module : link_module :=
    {|
      lm_cfun :=
        lcf serial_intr_disable f_serial_intr_disable_concrete ::
            lcf serial_intr_enable f_serial_intr_enable_concrete ::
            nil;
      lm_asmfun :=
        nil;
      lm_gvar :=
        nil
    |}.

  Definition DHandler_impl `{CompCertiKOS} `{RealParams} `{MultiOracleProp} `{WaitTime} :=
    link_impl DHandler_module dhandlerop.

End HandlerGenLinkSource.