The code used printf instead of the provided printf functions, resulting in strange output. Change-Id: I2c7c2531d8d54ecdea97e8c189d18d351320ca7d