Library mcertikos.mm.PTCommGenLinkSource

Require Import LinkSourceTemplate.
Require Import MPTOp.
Require Import MPTOpCSource.

Definition MPTCommon_module :=
  {|
    lm_cfun :=
      lcf pt_alloc_pde f_pt_alloc_pde ::
      
      lcf pt_init_comm f_pt_init_comm ::
      nil;
    lm_asmfun :=
      nil;
    lm_gvar :=
      nil
  |}.

Definition MPTCommon_impl `{CompCertiKOS} `{RealParams} `{MultiOracleProp} :=
  link_impl MPTCommon_module mptop.