Library mcertikos.mm.ALInitGenLinkSource

Require Import LinkSourceTemplate.
Require Import CDataTypes.
Require Import MContainer.
Require Import MContainerCSource.
Require Import ALInitGenAsmSource.

Definition MALInit_module: link_module :=
  {|
    lm_cfun :=
      lcf at_get f_at_get ::
      lcf is_norm f_is_norm ::
      lcf at_get_c f_at_get_c ::
      lcf at_set f_at_set ::
      lcf set_norm f_set_norm ::
      lcf at_set_c f_at_set_c ::
      lcf set_nps f_set_nps ::
      lcf get_nps f_get_nps ::
      nil;
    lm_asmfun :=
      laf acquire_lock_AT acquire_lock_AT_function ::
      laf release_lock_AT release_lock_AT_function ::
      nil;
    lm_gvar :=
      lgv AT_LOC at_loc_type ::
      lgv ATC_LOC atc_loc_type ::
      lgv NPS_LOC nps_loc_type ::
      nil
  |}.

Definition MALInit_impl `{CompCertiKOS} `{RealParams} `{MultiOracleProp} :=
  link_impl MALInit_module mcontainer.