Library mcertikos.proc.VMCSIntroGenLinkSource

Require Import LinkSourceTemplate.
Require Import VEPTInit.
Require Import VEPTInitCSource.
Require Import VMCSIntroGenAsmSource.

Definition VVMCSIntro_module: link_module :=
  {|
    lm_cfun :=
      lcf vmcs_get_revid f_vmcs_get_revid ::
      lcf vmcs_set_revid f_vmcs_set_revid ::
      lcf vmcs_get_abrtid f_vmcs_get_abrtid ::
      lcf vmcs_set_abrtid f_vmcs_set_abrtid ::
      nil;
    lm_asmfun :=
      laf vmcs_readz vmcs_readz_function ::
      laf vmcs_writez vmcs_writez_function ::
      laf vmcs_readz64 vmcs_readz64_function ::
      laf vmcs_writez64 vmcs_writez64_function ::
      
      laf vmcs_write_ident vmcs_write_ident_function ::
      laf rcr0 rcr0_function ::
      laf rcr3 rcr3_function ::
      laf rcr4 rcr4_function ::
      laf rdmsr rdmsr_function ::
      laf wrmsr wrmsr_function ::
      laf vmptrld vmptrld_function ::
      laf vmx_enable vmx_enable_function ::
      nil;
    lm_gvar :=
      lgv VMCS_LOC v_vmcs ::
      nil
  |}.

Definition VVMCSIntro_impl `{CompCertiKOS} `{RealParams} `{MultiOracleProp} :=
  link_impl VVMCSIntro_module eptinit.