Library mcertikos.virt.intel.EPTInitGenLinkSource
*********************************************************************** * * * 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 VEPTOp.
Require Import VEPTOpCSource.
Definition VEPTInit_module: link_module :=
{|
lm_cfun :=
lcf ept_gpa_to_hpa f_ept_gpa_to_hpa ::
lcf ept_mmap f_ept_mmap ::
lcf ept_set_permission f_ept_set_permission ::
nil;
lm_asmfun :=
nil;
lm_gvar :=
nil
|}.
Definition VEPTInit_impl `{CompCertiKOS} `{RealParams} :=
link_impl VEPTInit_module eptop.