#include "types.h"
__declspec(section ".init") extern void __init_hardware(void);
__declspec(section ".init") extern void __flush_cache(register void* address, register unsigned int size);
extern void __init_cpp(void);