/*
 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
 *
 * SPDX-License-Identifier: BSD-2-Clause
 */

#pragma once

#include <sel4/sel4_arch/simple_types.h>

typedef signed char seL4_Int8;
typedef signed short seL4_Int16;
typedef signed int seL4_Int32;

typedef unsigned char seL4_Uint8;
typedef unsigned short seL4_Uint16;
typedef unsigned int seL4_Uint32;