Library mcertikos.devdrivers.ConsoleBuffIntroGenLinkSource

Require Import LinkSourceTemplate.
Require Import MQTicketLock.
Require Import MQTicketLockCSource.

Require Import CDataTypes.

Definition DConsoleBuffIntro_module: link_module :=
  {|
    lm_cfun :=
      lcf cons_buf_init f_cons_buf_init ::
      lcf cons_buf_write f_cons_buf_write ::
      lcf cons_buf_read f_cons_buf_read ::
      lcf cons_buf_wpos f_cons_buf_wpos ::
      nil;
    lm_asmfun :=
      nil;
    lm_gvar :=
      lgv cons_buf_LOC cons_buf_loc_type ::
      nil
  |}.

Definition DConsoleBuffIntro_impl `{CompCertiKOS} `{RealParams} `{MultiOracleProp} `{WaitTime} `{WaitTime} :=
  link_impl DConsoleBuffIntro_module mqticketlock.