#include "stdio.h"

void xts_test_output_char(char a)
{
    printf("%c", a);
}