The C standard says that printf() has to return the number of characters
it has printed.

Change-Id: I0ef50b1d6766d140724ac0a2fa2c5d023431f984
Signed-off-by: Antonio Nino Diaz <antonio.ninodiaz@arm.com>