void read_from_stdin();