Library mcertikos.devdrivers.HandlerIntroGenLinkSource

Require Import LinkSourceTemplate.
Require Import DConsole.
Require Import DConsoleCSource.

Require Import CDataTypes.

Definition DHandlerIntro_module: link_module :=
  {|
    lm_cfun :=
          lcf intr_default_handler f_intr_default_handler ::
      nil;
    lm_asmfun :=
      nil;
    lm_gvar :=
      nil
  |}.

Definition DHandlerIntro_impl `{CompCertiKOS} `{RealParams} `{MultiOracleProp} `{WaitTime} :=
  link_impl DHandlerIntro_module dconsole.