blob: 93e209386553c0bfb15c4ca11b414a207f490c19 [file] [log] [blame]
/*
* Copyright 2018, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: BSD-2-Clause
*/
#pragma once
#include <sel4utils/sel4_arch/util.h>
#include <sel4utils/sel4_arch/vspace.h>