Library mcertikos.devdrivers.SerialGenLinkSource

Require Import LinkSourceTemplate.
Require Import DSerialIntro.
Require Import DSerialIntroCSource.

Definition DSerial_module: link_module :=
  {|
    lm_cfun :=
      lcf serial_init f_serial_init ::
      lcf serial_putc f_serial_putc ::
      lcf serial_getc f_serial_getc ::
      nil;
    lm_asmfun :=
      nil;
    lm_gvar :=
      nil
  |}.

Definition DSerial_impl `{CompCertiKOS} `{RealParams} `{MultiOracleProp} `{WaitTime} :=
  link_impl DSerial_module dserial_intro.