Library mcertikos.trap.DispatchGenLinkSource

Require Import LinkSourceTemplate.
Require Import TTrap.
Require Import TTrapCSource.

Require Import GlobalOracleProp.
Require Import SingleOracle.
Require Import SingleAbstractDataType.

Section WITHCOMPCERTIKOS.

  Definition TDispatch_module: link_module :=
    {|
      lm_cfun :=
        lcf syscall_dispatch_C f_syscall_dispatch_c ::
            
            nil;
      lm_asmfun :=
        nil;
      lm_gvar :=
        nil
    |}.

  Definition TDispatch_impl `{CompCertiKOS} `{SingleOracleProp} `{RealParams} `{MultiOracleProp} :=
    link_impl TDispatch_module ttrap.

End WITHCOMPCERTIKOS.