Library mcertikos.ipc.IPCIntroGenLinkSource

Require Import LinkSourceTemplate.
Require Import PHThread.
Require Import PHThreadCSource.
Require Import CDataTypes.
Require Import GlobalOracleProp.
Require Import SingleOracle.
Require Import SingleAbstractDataType.

Section WITHCERTIKOS.

  Definition PIPCIntro_module: link_module :=
    {|
      lm_cfun :=
        lcf syncsendto_chan_pre f_syncsendto_chan_pre::
            lcf tryreceive_chan f_tryreceive_chan ::
            nil;
      lm_asmfun :=
        nil;
      lm_gvar :=
        nil
    |}.


  Definition PIPCIntro_impl `{CompCertiKOS} `{SingleOracleProp} `{RealParams} `{MultiOracleProp} :=
    link_impl PIPCIntro_module phthread.

End WITHCERTIKOS.