Library mcertikos.proc.CVOpGenLinkSource

Require Import LinkSourceTemplate.
Require Import PCVIntro.
Require Import PCVIntroCSource.

Definition PCVOp_module: link_module :=
  {|
    lm_cfun :=
      lcf ipc_send_body f_ipc_send_body ::
      lcf ipc_receive_body f_ipc_receive_body ::
      lcf fifobbq_pool_init f_fifobbq_pool_init ::
      nil;
    lm_asmfun :=
      nil;
    lm_gvar :=
      nil
  |}.

Definition PCVOp_impl `{CompCertiKOS} `{RealParams} `{MultiOracleProp} :=
  link_impl PCVOp_module pcvintro.