Library mcertikos.proc.UCtxtIntroGenLinkSource

Require Import LinkSourceTemplate.
Require Import PQThread.
Require Import PQThreadCSource.
Require Import UCtxtIntroGenAsmSource.
Require Import CDataTypes.

Definition PUCtxtIntro_module: link_module :=
  {|
    lm_cfun :=
      lcf uctx_get f_uctx_get ::
          lcf uctx_set f_uctx_set ::
          lcf uctx_set_eip f_uctx_set_eip ::
          lcf save_uctx f_save_uctx ::
          nil;
    lm_asmfun :=
      laf restore_uctx restoreuctx_function ::
      laf elf_load elfload_function ::
      nil;
    lm_gvar :=
      lgv UCTX_LOC uctx_loc_type ::
          nil
  |}.

Definition PUCtxtIntro_impl `{CompCertiKOS} `{RealParams} `{MultiOracleProp} :=
  link_impl PUCtxtIntro_module pqthread.