diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
index 731e82bda9c..06d2d447424 100644
--- a/src/cbmc/cbmc_parse_options.cpp
+++ b/src/cbmc/cbmc_parse_options.cpp
@@ -71,7 +71,9 @@ Function: cbmc_parse_optionst::cbmc_parse_optionst
 cbmc_parse_optionst::cbmc_parse_optionst(int argc, const char **argv):
   parse_options_baset(CBMC_OPTIONS, argc, argv),
   xml_interfacet(cmdline),
-  language_uit("CBMC " CBMC_VERSION, cmdline)
+  language_uit(cmdline, ui_message_handler),
+  ui_message_handler(language_uit::get_ui_cmdline(cmdline),
+                       "CBMC " CBMC_VERSION)
 {
 }
   
@@ -93,7 +95,9 @@ ::cbmc_parse_optionst::cbmc_parse_optionst(
   const std::string &extra_options):
   parse_options_baset(CBMC_OPTIONS+extra_options, argc, argv),
   xml_interfacet(cmdline),
-  language_uit("CBMC " CBMC_VERSION, cmdline)
+  language_uit(cmdline, ui_message_handler),
+  ui_message_handler(language_uit::get_ui_cmdline(cmdline),
+                       "CBMC " CBMC_VERSION)
 {
 }
 
diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h
index 730c9bbe440..d59f9687b9d 100644
--- a/src/cbmc/cbmc_parse_options.h
+++ b/src/cbmc/cbmc_parse_options.h
@@ -72,6 +72,7 @@ class cbmc_parse_optionst:
     const std::string &extra_options);
 
 protected:
+  ui_message_handlert ui_message_handler;
   virtual void register_languages();
 
   virtual void get_command_line_options(optionst &options);
diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp
index 9db9a9ecead..52986e2f9c2 100644
--- a/src/goto-analyzer/goto_analyzer_parse_options.cpp
+++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp
@@ -62,7 +62,9 @@ Function: goto_analyzer_parse_optionst::goto_analyzer_parse_optionst
 
 goto_analyzer_parse_optionst::goto_analyzer_parse_optionst(int argc, const char **argv):
   parse_options_baset(GOTO_ANALYSER_OPTIONS, argc, argv),
-  language_uit("GOTO-ANALYSER " CBMC_VERSION, cmdline)
+  language_uit(cmdline, ui_message_handler),
+  ui_message_handler(language_uit::get_ui_cmdline(cmdline),
+                     "GOTO-ANALYZER " CBMC_VERSION)
 {
 }
   
diff --git a/src/goto-analyzer/goto_analyzer_parse_options.h b/src/goto-analyzer/goto_analyzer_parse_options.h
index 960239c37fc..a06afbae387 100644
--- a/src/goto-analyzer/goto_analyzer_parse_options.h
+++ b/src/goto-analyzer/goto_analyzer_parse_options.h
@@ -49,6 +49,7 @@ class goto_analyzer_parse_optionst:
   goto_analyzer_parse_optionst(int argc, const char **argv);
 
 protected:
+  ui_message_handlert ui_message_handler;
   get_goto_modelt goto_model;
 
   virtual void register_languages();
diff --git a/src/goto-cc/compile.cpp b/src/goto-cc/compile.cpp
index da00e5b9b70..b50d294d12a 100644
--- a/src/goto-cc/compile.cpp
+++ b/src/goto-cc/compile.cpp
@@ -736,7 +736,9 @@ Function: compilet::compilet
 \*******************************************************************/
 
 compilet::compilet(cmdlinet &_cmdline):
-  language_uit("goto-cc " CBMC_VERSION, _cmdline),
+  language_uit(_cmdline, ui_message_handler),
+  ui_message_handler(language_uit::get_ui_cmdline(_cmdline),
+                     "goto-cc " CBMC_VERSION),
   ns(symbol_table),
   cmdline(_cmdline)
 {
diff --git a/src/goto-cc/compile.h b/src/goto-cc/compile.h
index 73a38a2d603..24d6ff41744 100644
--- a/src/goto-cc/compile.h
+++ b/src/goto-cc/compile.h
@@ -20,6 +20,7 @@ Date: June 2006
 class compilet:public language_uit
 {
 public:
+  ui_message_handlert ui_message_handler;
   namespacet ns;
   goto_functionst compiled_functions;
   bool echo_file_name;
diff --git a/src/goto-cc/goto_cc_mode.cpp b/src/goto-cc/goto_cc_mode.cpp
index 47fc85240a9..0ad81b46dc8 100644
--- a/src/goto-cc/goto_cc_mode.cpp
+++ b/src/goto-cc/goto_cc_mode.cpp
@@ -34,7 +34,9 @@ Function: goto_cc_modet::goto_cc_modet
 \*******************************************************************/
 
 goto_cc_modet::goto_cc_modet(goto_cc_cmdlinet &_cmdline):
-  language_uit("goto-cc " CBMC_VERSION, _cmdline),
+  language_uit(_cmdline, ui_message_handler),
+  ui_message_handler(language_uit::get_ui_cmdline(_cmdline),
+                     "goto-cc " CBMC_VERSION),
   cmdline(_cmdline)
 {
   register_languages();
diff --git a/src/goto-cc/goto_cc_mode.h b/src/goto-cc/goto_cc_mode.h
index 4f4c2f8f49c..740e27cd8ac 100644
--- a/src/goto-cc/goto_cc_mode.h
+++ b/src/goto-cc/goto_cc_mode.h
@@ -30,6 +30,7 @@ class goto_cc_modet:public language_uit
   ~goto_cc_modet();
   
 protected:
+  ui_message_handlert ui_message_handler;
   void register_languages();
   goto_cc_cmdlinet &cmdline;
 };
diff --git a/src/goto-diff/goto_diff_base.cpp b/src/goto-diff/goto_diff_base.cpp
index a85a6017e25..1eeedc155f2 100644
--- a/src/goto-diff/goto_diff_base.cpp
+++ b/src/goto-diff/goto_diff_base.cpp
@@ -7,6 +7,7 @@ Author: Peter Schrammel
 \*******************************************************************/
 
 #include <util/i2string.h>
+#include <util/json_expr.h>
 
 #include "goto_diff.h"
 
@@ -126,7 +127,10 @@ void goto_difft::convert_function(
 {
   const goto_programt &program=
     goto_model2.goto_functions.function_map.at(function_name).body;
-  result["file"]=json_stringt(
-    id2string(program.instructions.begin()->source_location.get_file()));
+  if(!program.instructions.empty())
+  {
+    result["sourceLocation"]=
+      json(program.instructions.begin()->source_location);
+  }
   result["name"]=json_stringt(id2string(function_name));
 }
diff --git a/src/goto-diff/goto_diff_languages.cpp b/src/goto-diff/goto_diff_languages.cpp
index 833c87bdaef..14897c9a53d 100644
--- a/src/goto-diff/goto_diff_languages.cpp
+++ b/src/goto-diff/goto_diff_languages.cpp
@@ -19,11 +19,11 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <java_bytecode/java_bytecode_language.h>
 #endif
 
-#include "goto_diff_parse_options.h"
+#include "goto_diff_languages.h"
 
 /*******************************************************************\
 
-Function: goto_diff_parse_optionst::register_languages
+Function: goto_diff_languagest::register_languages
 
   Inputs:
 
@@ -33,7 +33,7 @@ Function: goto_diff_parse_optionst::register_languages
 
 \*******************************************************************/
 
-void goto_diff_parse_optionst::register_languages()
+void goto_diff_languagest::register_languages()
 {
   register_language(new_ansi_c_language);
   register_language(new_cpp_language);
diff --git a/src/goto-diff/goto_diff_languages.h b/src/goto-diff/goto_diff_languages.h
new file mode 100644
index 00000000000..e6e10db18b6
--- /dev/null
+++ b/src/goto-diff/goto_diff_languages.h
@@ -0,0 +1,32 @@
+/*******************************************************************\
+
+Module: GOTO-DIFF Languages
+
+Author: Peter Schrammel
+
+\*******************************************************************/
+
+#ifndef CPROVER_GOTO_DIFF_LANGUAGES_H
+#define CPROVER_GOTO_DIFF_LANGUAGES_H
+
+#include <langapi/language_ui.h>
+#include <goto-programs/goto_model.h>
+
+class goto_diff_languagest :
+  public language_uit
+{
+public:
+  explicit goto_diff_languagest(
+    const cmdlinet& cmdline,
+    ui_message_handlert &ui_message_handler) :
+  language_uit(cmdline, ui_message_handler)
+  {
+    register_languages();
+  }
+
+protected:
+  virtual void register_languages();
+
+};
+
+#endif
diff --git a/src/goto-diff/goto_diff_parse_options.cpp b/src/goto-diff/goto_diff_parse_options.cpp
index 707b3c65c04..9798337f9d3 100644
--- a/src/goto-diff/goto_diff_parse_options.cpp
+++ b/src/goto-diff/goto_diff_parse_options.cpp
@@ -62,7 +62,10 @@ Function: goto_diff_parse_optionst::goto_diff_parse_optionst
 
 goto_diff_parse_optionst::goto_diff_parse_optionst(int argc, const char **argv):
   parse_options_baset(GOTO_DIFF_OPTIONS, argc, argv),
-  language_uit("GOTO_DIFF " CBMC_VERSION, cmdline)
+  goto_diff_languagest(cmdline, ui_message_handler),
+  ui_message_handler(language_uit::get_ui_cmdline(cmdline), 
+    "GOTO-DIFF " CBMC_VERSION),
+  languages2(cmdline, ui_message_handler)
 {
 }
 
@@ -83,7 +86,10 @@ ::goto_diff_parse_optionst::goto_diff_parse_optionst(
   const char **argv,
   const std::string &extra_options):
   parse_options_baset(GOTO_DIFF_OPTIONS+extra_options, argc, argv),
-  language_uit("GOTO_DIFF " CBMC_VERSION, cmdline)
+  goto_diff_languagest(cmdline, ui_message_handler),
+  ui_message_handler(language_uit::get_ui_cmdline(cmdline), 
+    "GOTO-DIFF " CBMC_VERSION),
+  languages2(cmdline, ui_message_handler)
 {
 }
 
@@ -309,20 +315,27 @@ int goto_diff_parse_optionst::doit()
   //
   // Print a banner
   //
-  status() << "GOTO_DIFF version " CBMC_VERSION " "
+  status() << "GOTO-DIFF version " CBMC_VERSION " "
            << sizeof(void *)*8 << "-bit "
            << config.this_architecture() << " "
            << config.this_operating_system() << eom;
 
-  register_languages();
+  if(cmdline.args.size()!=2)
+  {
+    error() << "Please provide two programs to compare" << eom;
+    return 6;
+  }
 
   goto_modelt goto_model1, goto_model2;
 
-  int get_goto_programs_ret=
-    get_goto_programs(options, goto_model1, goto_model2);
-
-  if(get_goto_programs_ret!=-1)
-    return get_goto_programs_ret;
+  int get_goto_program_ret=
+    get_goto_program(options, *this, goto_model1);
+  if(get_goto_program_ret!=-1)
+    return get_goto_program_ret;
+  get_goto_program_ret=
+    get_goto_program(options, languages2, goto_model2);
+  if(get_goto_program_ret!=-1)
+    return get_goto_program_ret;
 
   if(cmdline.isset("show-goto-functions"))
   {
@@ -376,7 +389,7 @@ int goto_diff_parse_optionst::doit()
 
 /*******************************************************************\
 
-Function: goto_diff_parse_optionst::get_goto_programs
+Function: goto_diff_parse_optionst::get_goto_program
 
   Inputs:
 
@@ -386,33 +399,54 @@ Function: goto_diff_parse_optionst::get_goto_programs
 
 \*******************************************************************/
 
-int goto_diff_parse_optionst::get_goto_programs(
+int goto_diff_parse_optionst::get_goto_program(
   const optionst &options,
-  goto_modelt &goto_model1,
-  goto_modelt &goto_model2)
+  goto_diff_languagest &languages,
+  goto_modelt &goto_model)
 {
-  if(cmdline.args.size()!=2)
+  status() << "Reading program from `" << cmdline.args[0] << "'" << eom;
+
+  if(is_goto_binary(cmdline.args[0]))
   {
-    error() << "Please provide two programs to compare" << eom;
-    return 6;
+    if(read_goto_binary(cmdline.args[0],
+                        goto_model.symbol_table, goto_model.goto_functions,
+                        languages.get_message_handler()))
+      return 6;
+
+    config.set(cmdline);
+    config.set_from_symbol_table(goto_model.symbol_table);
+
+    // This one is done.
+    cmdline.args.erase(cmdline.args.begin());
   }
+  else
+  {
+    // This is a a workaround to make parse() think that there is only 
+    // one source file.
+    std::string arg2("");
+    if(cmdline.args.size()==2)
+    {
+      arg2 = cmdline.args[1];
+      cmdline.args.erase(--cmdline.args.end());
+    }
 
-  status() << "Reading GOTO program from `" << cmdline.args[0] << "'" << eom;
+    if(languages.parse()) return 6;
+    if(languages.typecheck()) return 6;
+    if(languages.final()) return 6;
 
-  if(read_goto_binary(cmdline.args[0],
-                      goto_model1.symbol_table, goto_model1.goto_functions,
-                      get_message_handler()))
-    throw 0;
+    // we no longer need any parse trees or language files
+    languages.clear_parse();
 
-  status() << "Reading GOTO program from `" << cmdline.args[1] << "'" << eom;
+    status() << "Generating GOTO Program" << eom;
 
-  if(read_goto_binary(cmdline.args[1],
-                      goto_model2.symbol_table, goto_model2.goto_functions,
-                      get_message_handler()))
-    throw 0;
+    goto_model.symbol_table=languages.symbol_table;
+    goto_convert(goto_model.symbol_table, goto_model.goto_functions,
+                 ui_message_handler);
 
-  config.set(cmdline);
-  config.set_from_symbol_table(goto_model2.symbol_table);
+    // if we had a second argument then we will handle it next
+    if(arg2!="")
+      cmdline.args[0]=arg2;
+  }
 
   return -1; // no error, continue
 }
diff --git a/src/goto-diff/goto_diff_parse_options.h b/src/goto-diff/goto_diff_parse_options.h
index 1c22801e7f8..1b979f744b4 100644
--- a/src/goto-diff/goto_diff_parse_options.h
+++ b/src/goto-diff/goto_diff_parse_options.h
@@ -16,6 +16,8 @@ Author: Peter Schrammel
 
 #include <goto-programs/goto_model.h>
 
+#include "goto_diff_languages.h"
+
 class goto_modelt;
 class optionst;
 
@@ -28,7 +30,7 @@ class optionst;
 
 class goto_diff_parse_optionst:
   public parse_options_baset,
-  public language_uit
+  public goto_diff_languagest
 {
 public:
   virtual int doit();
@@ -41,14 +43,15 @@ class goto_diff_parse_optionst:
     const std::string &extra_options);
 
 protected:
-  virtual void register_languages();
+  ui_message_handlert ui_message_handler;
+  goto_diff_languagest languages2;
 
   virtual void get_command_line_options(optionst &options);
 
-  virtual int get_goto_programs(
+  virtual int get_goto_program(
     const optionst &options,
-    goto_modelt &goto_model1,
-    goto_modelt &goto_model2);
+    goto_diff_languagest &languages,
+    goto_modelt &goto_model);
 
   virtual bool process_goto_program(
     const optionst &options,
diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h
index 3439edd52e2..f3197dad409 100644
--- a/src/goto-instrument/goto_instrument_parse_options.h
+++ b/src/goto-instrument/goto_instrument_parse_options.h
@@ -73,7 +73,8 @@ class goto_instrument_parse_optionst:
 
   goto_instrument_parse_optionst(int argc, const char **argv):
     parse_options_baset(GOTO_INSTRUMENT_OPTIONS, argc, argv),
-    language_uit("goto-instrument", cmdline),
+    language_uit(cmdline, ui_message_handler),
+    ui_message_handler(language_uit::get_ui_cmdline(cmdline),"goto-instrument"),
     function_pointer_removal_done(false),
     partial_inlining_done(false),
     remove_returns_done(false)
@@ -81,6 +82,7 @@ class goto_instrument_parse_optionst:
   }
   
 protected:
+  ui_message_handlert ui_message_handler;
   virtual void register_languages();
 
   void get_goto_program();
diff --git a/src/langapi/language_ui.cpp b/src/langapi/language_ui.cpp
index 2f68efd7ddb..4526fde9fc6 100644
--- a/src/langapi/language_ui.cpp
+++ b/src/langapi/language_ui.cpp
@@ -31,7 +31,7 @@ Function: get_ui_cmdline
 
 \*******************************************************************/
 
-static ui_message_handlert::uit get_ui_cmdline(const cmdlinet &cmdline)
+ui_message_handlert::uit language_uit::get_ui_cmdline(const cmdlinet &cmdline)
 {
   if(cmdline.isset("xml-ui"))
     return ui_message_handlert::XML_UI;
@@ -55,9 +55,9 @@ Function: language_uit::language_uit
 \*******************************************************************/
 
 language_uit::language_uit(
-  const std::string &program,
-  const cmdlinet &__cmdline):
-  ui_message_handler(get_ui_cmdline(__cmdline), program),
+  const cmdlinet &__cmdline,
+  ui_message_handlert &_ui_message_handler):
+  ui_message_handler(_ui_message_handler),
   _cmdline(__cmdline)
 {
   set_message_handler(ui_message_handler);
diff --git a/src/langapi/language_ui.h b/src/langapi/language_ui.h
index fecf19e15a7..1b7a58a25ab 100644
--- a/src/langapi/language_ui.h
+++ b/src/langapi/language_ui.h
@@ -22,9 +22,9 @@ class language_uit:public messaget
   language_filest language_files;
   symbol_tablet symbol_table;
   
-  language_uit(
-    const std::string &program,
-    const cmdlinet &__cmdline);
+  explicit language_uit(
+    const cmdlinet &__cmdline,
+    ui_message_handlert &ui_message_handler);
   virtual ~language_uit();
 
   virtual bool parse();
@@ -41,6 +41,8 @@ class language_uit:public messaget
   virtual void show_symbol_table_plain(std::ostream &out, bool brief);
   virtual void show_symbol_table_xml_ui(bool brief);
 
+  static ui_message_handlert::uit get_ui_cmdline(const cmdlinet &cmdline);
+
   typedef ui_message_handlert::uit uit;
   
   uit get_ui()
@@ -48,7 +50,7 @@ class language_uit:public messaget
     return ui_message_handler.get_ui();
   }
   
-  ui_message_handlert ui_message_handler;
+  ui_message_handlert &ui_message_handler;
 
 protected:
   const cmdlinet &_cmdline;
diff --git a/src/symex/symex_parse_options.cpp b/src/symex/symex_parse_options.cpp
index fd1d3809ca1..f3cee658ead 100644
--- a/src/symex/symex_parse_options.cpp
+++ b/src/symex/symex_parse_options.cpp
@@ -60,7 +60,9 @@ Function: symex_parse_optionst::symex_parse_optionst
 
 symex_parse_optionst::symex_parse_optionst(int argc, const char **argv):
   parse_options_baset(SYMEX_OPTIONS, argc, argv),
-  language_uit("Symex " CBMC_VERSION, cmdline)
+  language_uit(cmdline, ui_message_handler),
+  ui_message_handler(language_uit::get_ui_cmdline(cmdline),
+                     "Symex " CBMC_VERSION)
 {
 }
   
diff --git a/src/symex/symex_parse_options.h b/src/symex/symex_parse_options.h
index 379c522b062..8d27cd31bad 100644
--- a/src/symex/symex_parse_options.h
+++ b/src/symex/symex_parse_options.h
@@ -55,6 +55,7 @@ class symex_parse_optionst:
   symex_parse_optionst(int argc, const char **argv);
 
 protected:
+  ui_message_handlert ui_message_handler;
   get_goto_modelt goto_model;
 
   void get_command_line_options(optionst &options);