Listing 3

#define UART_TXBUF ((volatile uint32_t*) 0xfffe0004)
#define UART_TXCTL ((volatile uint8_t*)  0xfffe0001)
*UART_TXBUF = 10;
*UART_TXCTL = 3;