Library mcertikos.mm.PTKernGenLinkSource

Require Import LinkSourceTemplate.
Require Import MPTCommonCSource.
Require Import MPTCommon.

Definition MPTKern_module: link_module :=
  {|
    lm_cfun :=
      lcf pt_insert f_pt_insert ::
      lcf pt_rmv f_pt_rmv ::
      lcf pt_init_kern f_pt_init_kern ::
      nil;
    lm_asmfun :=
      nil;
    lm_gvar :=
      nil
  |}.

Definition MPTKern_impl `{CompCertiKOS} `{RealParams} `{MultiOracleProp} :=
  link_impl MPTKern_module mptcommon.