/*
 * Copyright 2017, Data61, CSIRO (ABN 41 687 119 230)
 *
 * SPDX-License-Identifier: BSD-2-Clause
 */
/* this file is shared between sel4test-driver an sel4test-tests */
#pragma once

#include <allocman/allocman.h>
#include <sel4/bootinfo.h>

#include <vka/vka.h>
#include <vka/object.h>
#include <sel4test/test.h>
#include <sel4platsupport/timer.h>
#include <sel4utils/api.h>
#include <simple/simple.h>
#include <vspace/vspace.h>

/* This file is a symlink to the original in sel4test-driver. */
#include <test_init_data.h>

void arch_init_simple(env_t env, simple_t *simple);