text: /*
   * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
   *
   * SPDX-License-Identifier: BSD-2-Clause
   */
  
  #pragma once
  typedef enum api_object {
      seL4_UntypedObject,
      seL4_TCBObject,
      seL4_EndpointObject,
      seL4_NotificationObject,
      seL4_CapTableObject,
  #ifdef CONFIG_KERNEL_MCS
      seL4_SchedContextObject,
      seL4_ReplyObject,
  #endif
      seL4_NonArchObjectTypeCount,
  } seL4_ObjectType;
  
  __attribute__((deprecated("use seL4_NotificationObject"))) static const seL4_ObjectType seL4_AsyncEndpointObject =
      seL4_NotificationObject;
  
  typedef seL4_Word api_object_t;
  
  