1 /*
2  * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3  *
4  * SPDX-License-Identifier: GPL-2.0-only
5  */
6 
7 #pragma once
8 #include <config.h>
9 #include <types.h>
10 #include <basic_types.h>
11 #include <linker.h>
12 #include <machine/io.h>
13 
14