Library mcertikos.proc.AbQueueAtomicGenLinkSource

Require Import LinkSourceTemplate.
Require Import PAbQueue.
Require Import PAbQueueCSource.

Definition PAbQueueAtomic_module: link_module :=
  {|
    lm_cfun :=
      lcf enqueue_atomic f_enqueue_atomic ::
      lcf dequeue_atomic f_dequeue_atomic ::
      nil;
    lm_asmfun :=
      nil;
    lm_gvar :=
      nil
  |}.

Definition PAbQueueAtomic_impl `{CompCertiKOS} `{RealParams} `{MultiOracleProp} :=
  link_impl PAbQueueAtomic_module pabqueue.