Library mcertikos.proc.VMCSInitGenLinkSource

Require Import LinkSourceTemplate.
Require Import VVMCSIntro.
Require Import VVMCSIntroCSource.

Definition VVMCSInit_module: link_module :=
  {|
    lm_cfun :=
      lcf vmx_set_intercept_intwin f_vmx_set_intercept_intwin ::
      lcf vmx_set_desc1 f_vmx_set_desc1 ::
      lcf vmx_set_desc2 f_vmx_set_desc2 ::
      lcf vmx_inject_event f_vmx_inject_event ::
      lcf vmx_set_tsc_offset f_vmx_set_tsc_offset ::
      lcf vmx_get_tsc_offset f_vmx_get_tsc_offset ::
      lcf vmx_get_exit_reason f_vmx_get_exit_reason ::
      lcf vmx_get_exit_fault_addr f_vmx_get_exit_fault_addr ::
      lcf vmx_check_pending_event f_vmx_check_pending_event ::
      lcf vmx_check_int_shadow f_vmx_check_int_shadow ::
      lcf vmcs_set_defaults f_vmcs_set_defaults ::
      nil;
    lm_asmfun :=
      nil;
    lm_gvar :=
      nil
  |}.

Definition VVMCSInit_impl `{CompCertiKOS} `{RealParams} `{MultiOracleProp} :=
  link_impl VVMCSInit_module vmcsintro.