Library mcertikos.mm.ContainerGenLinkSource

Require Import LinkSourceTemplate.
Require Import MContainerIntro.
Require Import MContainerIntroCSource.

Definition MContainer_module: link_module :=
  {|
    lm_cfun :=
      lcf container_init f_container_init ::
      lcf container_split f_container_split ::
      nil;
    lm_asmfun :=
      nil;
    lm_gvar :=
      nil
  |}.

Definition MContainer_impl `{CompCertiKOS} `{RealParams} `{MultiOracleProp} `{WaitTime} :=
  link_impl MContainer_module mcontainerintro.