#5645 False positive Null pointer derefence about first argument to fputc()