Library mcertikos.trap.TrapGenLinkSource

Require Import LinkSourceTemplate.
Require Import TTrapArg.
Require Import TTrapArgCSource.
Require Import TTrapArgCSource2.

Require Import GlobalOracleProp.
Require Import SingleOracle.

Require Import SingleAbstractDataType.

Section WITHCOMPCERTIKOS.


  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_sendto_chan f_sys_sendto_chan ::
            lcf sys_inject_event f_sys_inject_event ::
            lcf sys_check_int_shadow f_sys_check_int_shadow ::
            lcf sys_check_pending_event f_sys_check_pending_event ::
            lcf sys_intercept_int_window f_sys_set_intercept_intwin ::
            lcf sys_get_next_eip f_sys_get_next_eip ::
            lcf sys_get_reg f_sys_get_reg ::
            lcf sys_set_reg f_sys_set_reg ::
            lcf sys_set_seg1 f_sys_set_seg1 ::
            lcf sys_set_seg2 f_sys_set_seg2 ::
            lcf sys_get_tsc_offset f_sys_get_tsc_offset ::
            lcf sys_set_tsc_offset f_sys_set_tsc_offset ::
            lcf sys_get_exitinfo f_sys_get_exitinfo ::
            lcf sys_handle_rdmsr f_sys_handle_rdmsr ::
            lcf sys_handle_wrmsr f_sys_handle_wrmsr ::
            lcf sys_mmap f_sys_mmap ::
            lcf sys_getc f_sys_getc ::
            lcf sys_putc f_sys_putc ::
            nil;
      lm_asmfun :=
        nil;
      lm_gvar :=
        nil
    |}.

  Definition TTrap_impl `{CompCertiKOS} `{SingleOracleProp} `{RealParams} `{MultiOracleProp} :=
    link_impl TTrap_module ttraparg.

End WITHCOMPCERTIKOS.