/* Writes data to the specified GPIO data port.  */
void GPIO_WriteOutputPort(GPIO_T *port, uint16_t portValue)
/* Writes data to the specified GPIO data port.  */
void GPIO_WriteOutputPort(GPIO_T *port, uint16_t portValue)
{
    port->ODATA = (uint32_t)portValue;
}