Library mcertikos.devdrivers.HandlerSwGenLinkSource

Require Import LinkSourceTemplate.
Require Import DHandlerIntro.
Require Import DHandlerIntroCSource.

Require Import CDataTypes.

Definition DHandlerSw_module: link_module :=
  {|
    lm_cfun :=
      lcf serial_intr_handler_sw f_serial_intr_handler_sw ::
      nil;
    lm_asmfun :=
      nil;
    lm_gvar :=
      nil
  |}.

Definition DHandlerSw_impl `{CompCertiKOS} `{RealParams} `{MultiOracleProp} `{WaitTime} :=
  link_impl DHandlerSw_module dhandlerintro.