Library mcertikos.mm.ContainerIntroGenLinkSource

Require Import LinkSourceTemplate.
Require Import DAbsHandler.
Require Import DAbsHandlerCSource.
Require Import CDataTypes.

Definition MContainerIntro_module: link_module :=
  {|
    lm_cfun :=
      lcf container_node_init f_container_set_values ::
      lcf container_set_nchildren f_container_set_nchildren ::
      lcf container_set_usage f_container_set_usage ::
      lcf container_get_parent f_container_get_parent ::
      lcf container_get_nchildren f_container_get_nchildren ::
      lcf container_get_quota f_container_get_quota ::
      lcf container_get_usage f_container_get_usage ::
      lcf container_can_consume f_container_can_consume ::
      lcf container_alloc f_container_alloc ::
      nil;
    lm_asmfun :=
      nil;
    lm_gvar :=
      lgv AC_LOC container_loc_type ::
      nil
  |}.

Definition MContainerIntro_impl `{CompCertiKOS} `{RealParams} `{MultiOracleProp} `{WaitTime} :=
  link_impl MContainerIntro_module dabshandler.