Library mcertikos.proc.EPTIntroGenLinkSource

Require Import LinkSourceTemplate.
Require Import PProc.
Require Import PProcCSource.
Require Import EPTIntroGenAsmSource.

Definition VEPTIntro_module: link_module :=
  {|
    lm_cfun :=
      lcf get_EPTE f_get_EPTE ::
      lcf set_EPTE f_set_EPTE ::
      lcf set_EPDPTE f_set_EPDPTE ::
      lcf set_EPDTE f_set_EPDTE ::
      lcf set_EPML4E f_set_EPML4E ::
      nil;
    lm_asmfun :=
      laf ept_invalidate_mappings ept_invalidate_mappings_function ::
      nil;
    lm_gvar :=
      lgv EPT_LOC v_ept ::
      nil
  |}.

Definition VEPTIntro_impl `{CompCertiKOS} `{RealParams} `{MultiOracleProp} :=
  link_impl VEPTIntro_module pproc.