Library mcertikos.devdrivers.SerialIntroGenLinkSource

Require Import LinkSourceTemplate.
Require Import DAbsConsoleBuffIntro.
Require Import DAbsConsoleBuffIntroCSource.

Require Import CDataTypes.

Definition DSerialIntro_module: link_module :=
  {|
    lm_cfun :=
      lcf get_serial_exists f_get_serial_exists ::
      lcf set_serial_exists f_set_serial_exists ::
      nil;
    lm_asmfun :=
      nil;
    lm_gvar :=
      lgv serial_exists_LOC v_serial_exists ::
      nil
  |}.

Definition DSerialIntro_impl `{CompCertiKOS} `{RealParams} `{MultiOracleProp} `{WaitTime} :=
  link_impl DSerialIntro_module dabsconsolebuffintro.