Library mcertikos.devdrivers.LApicGenLinkSource

Require Import LinkSourceTemplate.
Require Import DIoApic.
Require Import DIoApicCSource.

Definition DLApic_module: link_module :=
  {|
    lm_cfun :=
      lcf lapic_init f_lapic_init ::
      lcf lapic_eoi f_lapic_eoi ::
      nil;
    lm_asmfun :=
      nil;
    lm_gvar :=
      nil
  |}.

Definition DLApic_impl `{CompCertiKOS} `{RealParams} `{MultiOracleProp} `{WaitTime} :=
  link_impl DLApic_module dioapic.