Library mcertikos.mm.ShareGenLinkSource

Require Import LinkSourceTemplate.
Require Import MShareOp.
Require Import MShareOpCSource.

Definition MShare_module: link_module :=
  {|
    lm_cfun :=
      lcf shared_mem_status f_shared_mem_status ::
      lcf offer_shared_mem f_offer_shared_mem ::
      nil;
    lm_asmfun :=
      nil;
    lm_gvar :=
      nil
  |}.

Definition MShare_impl `{CompCertiKOS} `{RealParams} `{MultiOracleProp} :=
  link_impl MShare_module mshareop.