Library mcertikos.trap.SysCallGenLinkSource

Require Import LinkSourceTemplate.
Require Import TDispatch.
Require Import SysCallGenAsmSource.

Require Import GlobalOracleProp.
Require Import SingleOracle.

Require Import SingleAbstractDataType.

Section WITHCOMPCERTIKOS.

  Definition TSysCall_module: link_module :=
    {|
      lm_cfun :=
        nil;
      lm_asmfun :=
        laf syscall_dispatch sys_dispatch_function ::
            laf pgf_handler pgf_handler_function ::
            
            laf sys_run_vm sys_run_vm_function ::
      nil;
      lm_gvar :=
      nil
    |}.

  Definition TSysCall_impl `{CompCertiKOS} `{SingleOracleProp} `{RealParams} `{MultiOracleProp} :=
    link_impl TSysCall_module tdispatch.

End WITHCOMPCERTIKOS.