Library mcertikos.devdrivers.IoApicGenLinkSource

Require Import LinkSourceTemplate.
Require Import DSerial.
Require Import DSerialCSource.

Definition DIoApic_module: link_module :=
  {|
    lm_cfun :=
      lcf ioapic_init f_ioapic_init ::
      lcf ioapic_enable f_ioapic_enable ::
      lcf ioapic_mask f_ioapic_mask ::
      lcf ioapic_unmask f_ioapic_unmask ::
      nil;
    lm_asmfun :=
      nil;
    lm_gvar :=
      nil
  |}.

Definition DIoApic_impl `{CompCertiKOS} `{RealParams} `{MultiOracleProp} `{WaitTime} :=
  link_impl DIoApic_module dserial.