Library mcertikos.trap.TrapArgGenLinkSource

Require Import LinkSourceTemplate.
Require Import PIPC.
Require Import PIPCCSource.
Require Import CDataTypes.
Require Import GlobalOracleProp.
Require Import SingleOracle.
Require Import SingleAbstractDataType.

Section WITHCOMPCERTIKOS.

  Definition TTrapArg_module: link_module :=
    {|
      lm_cfun :=
        lcf uctx_arg1 f_uctx_arg1::
            lcf uctx_arg2 f_uctx_arg2::
            lcf uctx_arg3 f_uctx_arg3::
            lcf uctx_arg4 f_uctx_arg4::
            lcf uctx_set_errno f_uctx_set_errno::
            lcf uctx_set_retval1 f_uctx_set_retval1::
            lcf uctx_set_retval2 f_uctx_set_retval2::
            lcf uctx_set_retval3 f_uctx_set_retval3::
            nil;
      lm_asmfun :=
        nil;
      lm_gvar :=
        nil
    |}.


  Definition TTrapArg_impl `{CompCertiKOS} `{SingleOracleProp} `{RealParams} `{MultiOracleProp} :=
    link_impl TTrapArg_module pipc.

End WITHCOMPCERTIKOS.