Library mcertikos.proc.ProcGenLinkSource

Require Import LinkSourceTemplate.
Require Import PUCtxtIntro.
Require Import PUCtxtIntroCSource.
Require Import ProcGenAsmSource.

Definition PProc_module: link_module :=
  {|
    lm_cfun :=
      lcf proc_create f_proc_create ::
          nil;
    lm_asmfun :=
      laf proc_start_user proc_start_user_function ::
          laf proc_exit_user proc_exit_user_function ::
          laf proc_start_user2 proc_start_user_function ::
          laf proc_exit_user2 proc_exit_user_function ::
          nil;
    lm_gvar :=
      nil
  |}.

Definition PProc_impl `{CompCertiKOS} `{RealParams} `{MultiOracleProp} :=
  link_impl PProc_module puctxtintro.