Library mcertikos.proc.VMXIntroGenLinkSource

Require Import LinkSourceTemplate.
Require Import VVMCSInit.
Require Import VVMCSInitCSource.
Require Import VMXIntroGenAsmSource.

Definition VVMXIntro_module: link_module :=
  {|
    lm_cfun :=
      lcf vmx_readz f_vmx_readz ::
      lcf vmx_writez f_vmx_writez ::
      lcf vmx_enter_pre f_vmx_enter_pre ::
      lcf vmx_exit_post f_vmx_exit_post ::
      nil;
    lm_asmfun :=
      laf vmx_enter vmx_enter_function ::
      laf vmx_exit vmx_exit_function ::
      nil;
    lm_gvar :=
      lgv VMX_LOC v_VMX_LOC ::
      nil
  |}.

Definition VVMXIntro_impl `{CompCertiKOS} `{RealParams} `{MultiOracleProp} :=
  link_impl VVMXIntro_module vmcsinit.