#include <stdint.h>

/* Declare the I/O registers.  */
extern volatile __regio_symbol uint32_t __R30;
extern volatile __regio_symbol uint32_t __R31;