Library mcertikos.ticketlog.CurIDGenLinkSource

Require Import LinkSourceTemplate.
Require Import CDataTypes.
Require Import MBoot.
Require Import MBootCSource.

Definition MCurID_module: link_module :=
  {|
    lm_cfun :=
      lcf get_curid f_get_curid ::
      lcf set_curid f_set_curid ::
      lcf set_curid_init f_set_curid_init ::
      nil;
    lm_asmfun :=
      nil;
    lm_gvar :=
      lgv CURID_LOC curid_loc_type ::
      nil
  |}.

Definition MCurID_impl `{CompCertiKOS} `{RealParams} `{MultiOracleProp} :=
  link_impl MCurID_module mboot.