Library mcertikos.virt.intel.EPTIntroGenLinkSource
*********************************************************************** * * * 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 PProc.
Require Import PProcCSource.
Definition VEPTIntro_module: link_module :=
{|
lm_cfun :=
lcf get_EPTE f_get_EPTE ::
lcf set_EPTE f_set_EPTE ::
lcf set_EPDPTE f_set_EPDPTE ::
lcf set_EPDTE f_set_EPDTE ::
lcf set_EPML4E f_set_EPML4E ::
nil;
lm_asmfun :=
nil;
lm_gvar :=
lgv EPT_LOC v_ept ::
nil
|}.
Definition VEPTIntro_impl `{CompCertiKOS} `{RealParams} :=
link_impl VEPTIntro_module pproc.