Library mcertikos.virt.intel.EPTOpGenLinkSource
*********************************************************************** * * * 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 VEPTIntro.
Require Import VEPTIntroCSource.
Require Import EPTOpGenAsmSource.
Definition VEPTOp_module: link_module :=
{|
lm_cfun :=
lcf ept_get_page_entry f_ept_get_page_entry ::
lcf ept_set_page_entry f_ept_set_page_entry ::
lcf ept_add_mapping f_ept_add_mapping ::
lcf ept_init f_ept_init ::
nil;
lm_asmfun :=
laf ept_invalidate_mappings ept_invalidate_mappings_function ::
nil;
lm_gvar :=
nil
|}.
Definition VEPTOp_impl `{CompCertiKOS} `{RealParams} :=
link_impl VEPTOp_module eptintro.