Library mcertikos.mm.ShareIntroGenLinkSource

Require Import LinkSourceTemplate.
Require Import MPTNew.
Require Import MPTNewCSource.

Definition MShareIntro_module: link_module :=
  {|
    lm_cfun :=
      lcf clear_shared_mem f_clear_shared_mem ::
      lcf get_shared_mem_state f_get_shared_mem_state ::
      lcf get_shared_mem_seen f_get_shared_mem_seen ::
      lcf get_shared_mem_loc f_get_shared_mem_loc ::
      lcf set_shared_mem_state f_set_shared_mem_state ::
      lcf set_shared_mem_seen f_set_shared_mem_seen ::
      lcf set_shared_mem_loc f_set_shared_mem_loc ::
      nil;
    lm_asmfun :=
      nil;
    lm_gvar :=
      lgv SHRDMEMPOOL_LOC smspool_loc_type ::
      nil
  |}.

Definition MShareIntro_impl `{CompCertiKOS} `{RealParams} `{MultiOracleProp} :=
  link_impl MShareIntro_module mptnew.