CL prints the name of the file that's compiled onto stdout

Author: Daniel Kroening

regression/goto-cl/echo-file/echo-file.desc

@@ -0,0 +1,9 @@
+CORE
+some_funny_file.c
+
+^EXIT=0$
+^SIGNAL=0$
+^some_funny_file.c$
+--
+^warning: ignoring
+^CONVERSION ERROR$

regression/goto-cl/echo-file/some_funny_file.c

@@ -0,0 +1,3 @@
+int main()
+{
+}

src/goto-cc/compile.cpp

@@ -391,8 +391,9 @@ bool compilet::compile()
     source_files.pop_front();
 
     // Visual Studio always prints the name of the file it's doing
+    // onto stdout. The name of the directory is stripped.
     if(echo_file_name)
-      status() << file_name << eom;
+      std::cout << get_base_name(file_name, false) << '\n' << std::flush;
 
     bool r=parse_source(file_name); // don't break the program!