The function getchar() returns an 'int' and not a 'char'. Coverity notes
that "Assigning the return value of getchar to char ... truncates its value."
and so for the most part we can resolve this easily by using 'int' as
intended, and often used throughout the codebase. A few places are not
so simple and would require further re-architecting of the code in order
to change this, so we leave them be.