Library mcertikos.proc.IPCGenLinkSource

Require Import LinkSourceTemplate.
Require Import PIPCIntro.
Require Import PIPCIntroCSource.

Definition PIPC_module: link_module :=
  {|
    lm_cfun :=
      lcf syncreceive_chan f_syncreceive_chan ::
      lcf syncsendto_chan_pre f_syncsendto_chan_pre ::
      lcf syncsendto_chan_post f_syncsendto_chan_post ::
      lcf proc_init f_proc_init ::
      nil;
    lm_asmfun :=
      nil;
    lm_gvar :=
      nil
  |}.

Definition PIPC_impl `{CompCertiKOS} `{RealParams} :=
  link_impl PIPC_module pipcintro.