Library mcertikos.proc.EPTOpGenLinkSource

Require Import LinkSourceTemplate.
Require Import VEPTIntro.
Require Import VEPTIntroCSource.

Definition VEPTOp_module: link_module :=
  {|
    lm_cfun :=
      lcf ept_get_page_entry f_ept_get_page_entry ::
      lcf ept_set_page_entry f_ept_set_page_entry ::
      lcf ept_add_mapping f_ept_add_mapping ::
      lcf ept_init f_ept_init ::
      nil;
    lm_asmfun :=
      nil;
    lm_gvar :=
      nil
  |}.

Definition VEPTOp_impl `{CompCertiKOS} `{RealParams} `{MultiOracleProp} :=
  link_impl VEPTOp_module eptintro.