Library mcertikos.proc.EPTInitGenLinkSource

Require Import LinkSourceTemplate.
Require Import VEPTOp.
Require Import VEPTOpCSource.

Definition VEPTInit_module: link_module :=
  {|
    lm_cfun :=
      lcf ept_gpa_to_hpa f_ept_gpa_to_hpa ::
      lcf ept_mmap f_ept_mmap ::
      lcf ept_set_permission f_ept_set_permission ::
      nil;
    lm_asmfun :=
      nil;
    lm_gvar :=
      nil
  |}.

Definition VEPTInit_impl `{CompCertiKOS} `{RealParams} `{MultiOracleProp} :=
  link_impl VEPTInit_module eptop.