Library mcertikos.mcslock.MCSCurIDGenLinkSource

Require Import LinkSourceTemplate.
Require Import CDataTypes.
Require Import MCSMBoot.
Require Import MCSMBootCSource.

Definition MCSMCurID_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 MCSMCurID_impl `{CompCertiKOS} `{RealParams} `{MCSOracleProp} :=
  link_impl MCSMCurID_module mboot.