Library mcertikos.proc.VMXInitGenLinkSource

Require Import LinkSourceTemplate.
Require Import VVMXIntro.
Require Import VVMXIntroCSource.
Require Import VMXInitGenAsmSource.

Definition VVMXInit_module: link_module :=
  {|
    lm_cfun :=
      lcf vmx_get_reg f_vmx_get_reg ::
      lcf vmx_set_reg f_vmx_set_reg ::
      lcf vmx_get_next_eip f_vmx_get_next_eip ::
      lcf vmx_get_io_width f_vmx_get_io_width ::
      lcf vmx_get_io_write f_vmx_get_io_write ::
      lcf vmx_get_exit_qualification f_vmx_get_exit_qualification ::
      lcf vmx_get_exit_io_rep f_vmx_get_exit_io_rep ::
      lcf vmx_get_exit_io_str f_vmx_get_exit_io_str ::
      lcf vmx_get_exit_io_port f_vmx_get_exit_io_port ::
      lcf vmx_set_mmap f_vmx_set_mmap ::
      lcf vmx_init f_vmx_init ::
      nil;
    lm_asmfun :=
      laf vmx_run_vm vm_run_function ::
      laf vmx_return_from_guest vmx_return_from_guest_function ::
      nil;
    lm_gvar :=
      nil
  |}.

Definition VVMXInit_impl `{CompCertiKOS} `{RealParams} `{MultiOracleProp} :=
  link_impl VVMXInit_module vmxintro.