Library mcertikos.proc.SleeperGenLinkSource

Require Import LinkSourceTemplate.
Require Import PKContextNew.
Require Import PKContextNewCSource.
Require Import CDataTypes.

Definition PSleeper_module: link_module :=
  {|
    lm_cfun :=
      lcf sleeper_inc f_sleeper_inc ::
      lcf sleeper_dec f_sleeper_dec ::
      lcf sleeper_zzz f_sleeper_zzz ::
      nil;
    lm_asmfun :=
      nil;
    lm_gvar :=
      lgv SLEEPER_LOC sleeper_loc_type ::
      nil
  |}.

Definition PSleeper_impl `{CompCertiKOS} `{RealParams} `{MultiOracleProp} :=
  link_impl PSleeper_module pkcontextnew.