Library mcertikos.devdrivers.ConsoleGenLinkSource

Require Import LinkSourceTemplate.
Require Import DLApic.
Require Import DLApicCSource.

Definition DConsole_module: link_module :=
  {|
    lm_cfun :=
      lcf cons_init f_cons_init ::
      lcf cons_intr f_cons_intr ::
      nil;
    lm_asmfun :=
      nil;
    lm_gvar :=
      nil
  |}.

Definition DConsole_impl `{CompCertiKOS} `{RealParams} `{MultiOracleProp} `{WaitTime} :=
  link_impl DConsole_module dlapic.