#include "device_registers.h"
#undef RCC
#undef GPIOA
#undef GPIOB
#undef GPIOF
#undef TIM1
#undef SPI2
extern RCC_TypeDef rcc;
extern GPIO_TypeDef ga,gb,gf;
extern TIM_TypeDef timer;
extern SPI_TypeDef spi;
#define RCC (&rcc)
#define GPIOA (&ga)
#define GPIOB (&gb)
#define GPIOF (&gf)
#define TIM1 (&timer)
#define SPI2 (&spi)
#ifdef HOST_INTEGRATED
void host_dsb(void);
void host_wait(void);
#define __DSB() host_dsb()
#define __WFI() host_wait()
#else
#define __DSB() ((void)0)
#endif
