Library mcertikos.trap.TrapGenLinkSource
Require Import LinkSourceTemplate.
Require Import TTrapArg.
Require Import TTrapArgCSource.
Definition TTrap_module: link_module :=
{|
lm_cfun :=
lcf ptfault_resv f_ptfault_resv ::
lcf sys_proc_create f_sys_proc_create ::
lcf sys_get_quota f_sys_get_quota ::
lcf sys_receive_chan f_sys_receive_chan ::
lcf sys_offer_shared_mem f_sys_offer_shared_mem ::
lcf print f_print ::
nil;
lm_asmfun :=
nil;
lm_gvar :=
nil
|}.
Definition TTrap_impl `{CompCertiKOS} `{RealParams} :=
link_impl TTrap_module ttraparg.
Require Import TTrapArg.
Require Import TTrapArgCSource.
Definition TTrap_module: link_module :=
{|
lm_cfun :=
lcf ptfault_resv f_ptfault_resv ::
lcf sys_proc_create f_sys_proc_create ::
lcf sys_get_quota f_sys_get_quota ::
lcf sys_receive_chan f_sys_receive_chan ::
lcf sys_offer_shared_mem f_sys_offer_shared_mem ::
lcf print f_print ::
nil;
lm_asmfun :=
nil;
lm_gvar :=
nil
|}.
Definition TTrap_impl `{CompCertiKOS} `{RealParams} :=
link_impl TTrap_module ttraparg.