Library mcertikos.virt.intel.VMXIntroGenLinkSource
*********************************************************************** * * * The CertiKOS Certified Kit Operating System * * * * The FLINT Group, Yale University * * * * Copyright The FLINT Group, Yale University. All rights reserved. * * This file is distributed under the terms of the Yale University * * Non-Commercial License Agreement. * * * ***********************************************************************
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} :=
link_impl VVMXIntro_module vmcsinit.