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.