diff --git a/appveyor.yml b/appveyor.yml
index 4f28cf54254..dff05f85412 100644
--- a/appveyor.yml
+++ b/appveyor.yml
@@ -74,6 +74,21 @@ test_script:
     sed -i "13i mv $NAME.exe $NAME.gb" goto-instrument-typedef/chain.sh || true
     cat goto-instrument-typedef/chain.sh || true
 
+    sed -i "s/goto-cc\/goto-cc/goto-cc\/goto-cl/" goto-cc-cbmc/chain.sh || true
+    sed -i "11s/.*/$GC $NAME.c/" goto-cc-cbmc/chain.sh || true
+    sed -i "12i mv $NAME.exe $NAME.gb" goto-cc-cbmc/chain.sh || true
+    cat goto-cc-cbmc/chain.sh || true
+
+    sed -i "s/goto-cc\/goto-cc/goto-cc\/goto-cl/" goto-cc-goto-analyzer/chain.sh || true
+    sed -i "11s/.*/$gc $name.c/" goto-cc-goto-analyzer/chain.sh || true
+    sed -i "12i mv $name.exe $name.gb" goto-cc-goto-analyzer/chain.sh || true
+    cat goto-cc-goto-analyzer/chain.sh || true
+
+    sed -i "s/goto-cc\/goto-cc/goto-cc\/goto-cl/" goto-cc-symex/chain.sh || true
+    sed -i "11s/.*/$gc $name.c/" goto-cc-symex/chain.sh || true
+    sed -i "12i mv $name.exe $name.gb" goto-cc-symex/chain.sh || true
+    cat goto-cc-symex/chain.sh || true
+
     rem HACK disable failing tests
     rmdir /s /q ansi-c\arch_flags_mcpu_bad
     rmdir /s /q ansi-c\arch_flags_mcpu_good
diff --git a/regression/Makefile b/regression/Makefile
index f4d37f8c442..0e791995ec2 100644
--- a/regression/Makefile
+++ b/regression/Makefile
@@ -5,6 +5,9 @@ DIRS = ansi-c \
        cbmc-java-inheritance \
        cpp \
        goto-analyzer \
+       goto-cc-cbmc \
+       goto-cc-goto-analyzer \
+       goto-cc-goto-symex \
        goto-diff \
        goto-gcc \
        goto-instrument \
diff --git a/regression/cbmc/pointer-function-parameters-2/test.desc b/regression/cbmc/pointer-function-parameters-2/test.desc
index c67211d7387..be81dbdc393 100644
--- a/regression/cbmc/pointer-function-parameters-2/test.desc
+++ b/regression/cbmc/pointer-function-parameters-2/test.desc
@@ -4,9 +4,9 @@ main.c
 ^\*\* 7 of 7 covered \(100.0%\)$
 ^\*\* Used 4 iterations$
 ^Test suite:$
-^a=\(\(signed int \*\*\)NULL\), tmp\$1=[^,]*, tmp\$2=[^,]*$
-^a=&tmp\$1!0, tmp\$1=\(\(signed int \*\)NULL\), tmp\$2=[^,]*$
-^a=&tmp\$1!0, tmp\$1=&tmp\$2!0, tmp\$2=([012356789][0-9]*|4[0-9]+)$
-^a=&tmp\$1!0, tmp\$1=&tmp\$2!0, tmp\$2=4$
+^a=\(\(signed int \*\*\)NULL\), tmp\$\d+=[^,]*, tmp\$\d+=[^,]*$
+^a=&tmp\$\d+!0, tmp\$\d+=\(\(signed int \*\)NULL\), tmp\$\d+=[^,]*$
+^a=&tmp\$\d+!0, tmp\$\d+=&tmp\$\d+!0, tmp\$\d+=([012356789][0-9]*|4[0-9]+)$
+^a=&tmp\$\d+!0, tmp\$\d+=&tmp\$\d+!0, tmp\$\d+=4$
 --
 ^warning: ignoring
diff --git a/regression/cbmc/pointer-function-parameters/test.desc b/regression/cbmc/pointer-function-parameters/test.desc
index b9aa6240dea..89fbd70531a 100644
--- a/regression/cbmc/pointer-function-parameters/test.desc
+++ b/regression/cbmc/pointer-function-parameters/test.desc
@@ -4,8 +4,8 @@ main.c
 ^\*\* 5 of 5 covered \(100\.0%\)$
 ^\*\* Used 3 iterations$
 ^Test suite:$
-^a=\(\(signed int \*\)NULL\), tmp\$1=[^,]*$
-^a=&tmp\$1!0, tmp\$1=4$
-^a=&tmp\$1!0, tmp\$1=([012356789][0-9]*|4[0-9]+)$
+^a=\(\(signed int \*\)NULL\), tmp\$\d+=[^,]*$
+^a=&tmp\$\d+!0, tmp\$\d+=4$
+^a=&tmp\$\d+!0, tmp\$\d+=([012356789][0-9]*|4[0-9]+)$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/regenerate-entry-function/main.c b/regression/goto-analyzer/regenerate-entry-function/main.c
new file mode 100644
index 00000000000..6a035127022
--- /dev/null
+++ b/regression/goto-analyzer/regenerate-entry-function/main.c
@@ -0,0 +1,16 @@
+#include <assert.h>
+
+int fun(int x)
+{
+	int i;
+	if(i>=20)
+    assert(i>=10);
+}
+
+int main(int argc, char** argv)
+{
+  int i;
+
+  if(i>=5)
+    assert(i>=10);
+}
diff --git a/regression/goto-analyzer/regenerate-entry-function/test.desc b/regression/goto-analyzer/regenerate-entry-function/test.desc
new file mode 100644
index 00000000000..289b7cbd276
--- /dev/null
+++ b/regression/goto-analyzer/regenerate-entry-function/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--function fun --show-goto-functions
+^\s*fun\(x\);$
+^EXIT=6$
+^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/regression/goto-cc-cbmc/Makefile b/regression/goto-cc-cbmc/Makefile
new file mode 100644
index 00000000000..191f99fcba1
--- /dev/null
+++ b/regression/goto-cc-cbmc/Makefile
@@ -0,0 +1,30 @@
+default: tests.log
+
+test:
+	@if ! ../test.pl -c ../chain.sh ; then \
+		../failed-tests-printer.pl ; \
+		exit 1; \
+	fi
+
+tests.log:
+	@if ! ../test.pl -c ../chain.sh ; then \
+		../failed-tests-printer.pl ; \
+		exit 1; \
+	fi
+
+show:
+	@for dir in *; do \
+		if [ -d "$$dir" ]; then \
+			vim -o "$$dir/*.c" "$$dir/*.out"; \
+		fi; \
+	done;
+
+clean:
+	@for dir in *; do \
+		$(RM) tests.log; \
+		if [ -d "$$dir" ]; then \
+			cd "$$dir"; \
+			$(RM) *.out *.gb; \
+			cd ..; \
+		fi \
+	done
diff --git a/regression/goto-cc-cbmc/chain.sh b/regression/goto-cc-cbmc/chain.sh
new file mode 100755
index 00000000000..1440e03272d
--- /dev/null
+++ b/regression/goto-cc-cbmc/chain.sh
@@ -0,0 +1,12 @@
+#!/bin/bash
+
+SRC=../../../src
+
+GC=$SRC/goto-cc/goto-cc
+CBMC=$SRC/cbmc/cbmc
+
+OPTS=$1
+NAME=${2%.c}
+
+$GC $NAME.c -o $NAME.gb
+$CBMC $NAME.gb $OPTS
diff --git a/regression/goto-cc-cbmc/regenerate-entry-function/main.c b/regression/goto-cc-cbmc/regenerate-entry-function/main.c
new file mode 100644
index 00000000000..644ef1eb086
--- /dev/null
+++ b/regression/goto-cc-cbmc/regenerate-entry-function/main.c
@@ -0,0 +1,23 @@
+int fun(int x)
+{
+	if(x > 0)
+	{
+		return x * x;
+	}
+	else
+	{
+		return x;
+	}
+}
+
+int main(int argc, char** argv)
+{
+	if(argc>4)
+	{
+		return 0;
+	}
+	else
+	{
+		return 1;
+	}
+}
diff --git a/regression/goto-cc-cbmc/regenerate-entry-function/test.desc b/regression/goto-cc-cbmc/regenerate-entry-function/test.desc
new file mode 100644
index 00000000000..ced965563f8
--- /dev/null
+++ b/regression/goto-cc-cbmc/regenerate-entry-function/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+"--function fun --cover branch"
+^EXIT=0$
+^SIGNAL=0$
+^x=
+--
+^warning: ignoring
diff --git a/regression/goto-cc-goto-analyzer/Makefile b/regression/goto-cc-goto-analyzer/Makefile
new file mode 100644
index 00000000000..18f4d370eb8
--- /dev/null
+++ b/regression/goto-cc-goto-analyzer/Makefile
@@ -0,0 +1,32 @@
+
+default: tests.log
+
+test:
+	@if ! ../test.pl -c ../chain.sh ; then \
+		../failed-tests-printer.pl ; \
+		exit 1; \
+	fi
+
+tests.log:
+	pwd
+	@if ! ../test.pl -c ../chain.sh ; then \
+		../failed-tests-printer.pl ; \
+		exit 1; \
+	fi
+
+show:
+	@for dir in *; do \
+		if [ -d "$$dir" ]; then \
+			vim -o "$$dir/*.c" "$$dir/*.out"; \
+		fi; \
+	done;
+
+clean:
+	@for dir in *; do \
+		rm -f tests.log; \
+		if [ -d "$$dir" ]; then \
+			cd "$$dir"; \
+			rm -f *.out *.gb; \
+			cd ..; \
+		fi \
+	done
diff --git a/regression/goto-cc-goto-analyzer/chain.sh b/regression/goto-cc-goto-analyzer/chain.sh
new file mode 100755
index 00000000000..b34d0e7750e
--- /dev/null
+++ b/regression/goto-cc-goto-analyzer/chain.sh
@@ -0,0 +1,12 @@
+#!/bin/bash
+
+src=../../../src
+
+gc=$src/goto-cc/goto-cc
+goto_analyzer=$src/goto-analyzer/goto-analyzer
+
+options=$1
+name=${2%.c}
+
+$gc $name.c -o $name.gb
+$goto_analyzer $name.gb $options
diff --git a/regression/goto-cc-goto-analyzer/regenerate-entry-function/main.c b/regression/goto-cc-goto-analyzer/regenerate-entry-function/main.c
new file mode 100644
index 00000000000..6a035127022
--- /dev/null
+++ b/regression/goto-cc-goto-analyzer/regenerate-entry-function/main.c
@@ -0,0 +1,16 @@
+#include <assert.h>
+
+int fun(int x)
+{
+	int i;
+	if(i>=20)
+    assert(i>=10);
+}
+
+int main(int argc, char** argv)
+{
+  int i;
+
+  if(i>=5)
+    assert(i>=10);
+}
diff --git a/regression/goto-cc-goto-analyzer/regenerate-entry-function/test.desc b/regression/goto-cc-goto-analyzer/regenerate-entry-function/test.desc
new file mode 100644
index 00000000000..0dd59956634
--- /dev/null
+++ b/regression/goto-cc-goto-analyzer/regenerate-entry-function/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+"--function fun --show-goto-functions"
+^\s*fun\(x\);$
+^EXIT=6$
+^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/regression/goto-cc-symex/Makefile b/regression/goto-cc-symex/Makefile
new file mode 100644
index 00000000000..18f4d370eb8
--- /dev/null
+++ b/regression/goto-cc-symex/Makefile
@@ -0,0 +1,32 @@
+
+default: tests.log
+
+test:
+	@if ! ../test.pl -c ../chain.sh ; then \
+		../failed-tests-printer.pl ; \
+		exit 1; \
+	fi
+
+tests.log:
+	pwd
+	@if ! ../test.pl -c ../chain.sh ; then \
+		../failed-tests-printer.pl ; \
+		exit 1; \
+	fi
+
+show:
+	@for dir in *; do \
+		if [ -d "$$dir" ]; then \
+			vim -o "$$dir/*.c" "$$dir/*.out"; \
+		fi; \
+	done;
+
+clean:
+	@for dir in *; do \
+		rm -f tests.log; \
+		if [ -d "$$dir" ]; then \
+			cd "$$dir"; \
+			rm -f *.out *.gb; \
+			cd ..; \
+		fi \
+	done
diff --git a/regression/goto-cc-symex/chain.sh b/regression/goto-cc-symex/chain.sh
new file mode 100755
index 00000000000..25217b24e2a
--- /dev/null
+++ b/regression/goto-cc-symex/chain.sh
@@ -0,0 +1,12 @@
+#!/bin/bash
+
+src=../../../src
+
+gc=$src/goto-cc/goto-cc
+symex=$src/symex/symex
+
+options=$1
+name=${2%.c}
+
+$gc $name.c -o $name.gb
+$symex $name.gb $options
diff --git a/regression/goto-cc-symex/regenerate-entry-function/main.c b/regression/goto-cc-symex/regenerate-entry-function/main.c
new file mode 100644
index 00000000000..6a035127022
--- /dev/null
+++ b/regression/goto-cc-symex/regenerate-entry-function/main.c
@@ -0,0 +1,16 @@
+#include <assert.h>
+
+int fun(int x)
+{
+	int i;
+	if(i>=20)
+    assert(i>=10);
+}
+
+int main(int argc, char** argv)
+{
+  int i;
+
+  if(i>=5)
+    assert(i>=10);
+}
diff --git a/regression/goto-cc-symex/regenerate-entry-function/test.desc b/regression/goto-cc-symex/regenerate-entry-function/test.desc
new file mode 100644
index 00000000000..709ad39e859
--- /dev/null
+++ b/regression/goto-cc-symex/regenerate-entry-function/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+"--function fun --show-goto-functions"
+^\s*return.=fun\(x\);$
+^EXIT=6$
+^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/regression/symex/regenerate-entry-function/main.c b/regression/symex/regenerate-entry-function/main.c
new file mode 100644
index 00000000000..6a035127022
--- /dev/null
+++ b/regression/symex/regenerate-entry-function/main.c
@@ -0,0 +1,16 @@
+#include <assert.h>
+
+int fun(int x)
+{
+	int i;
+	if(i>=20)
+    assert(i>=10);
+}
+
+int main(int argc, char** argv)
+{
+  int i;
+
+  if(i>=5)
+    assert(i>=10);
+}
diff --git a/regression/symex/regenerate-entry-function/test.desc b/regression/symex/regenerate-entry-function/test.desc
new file mode 100644
index 00000000000..722900f544e
--- /dev/null
+++ b/regression/symex/regenerate-entry-function/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--function fun --show-goto-functions
+fun\(x\);$
+^EXIT=6$
+^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/regression/symex/show-trace1/test.desc b/regression/symex/show-trace1/test.desc
index 930f344a07a..23a9f62e3ae 100644
--- a/regression/symex/show-trace1/test.desc
+++ b/regression/symex/show-trace1/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --trace
 ^EXIT=10$
@@ -9,3 +9,5 @@ main.c
 ^  k=6 .*$
 --
 ^warning: ignoring
+--
+diffblue/cbmc#1361
\ No newline at end of file
diff --git a/src/ansi-c/ansi_c_entry_point.cpp b/src/ansi-c/ansi_c_entry_point.cpp
index af1f6c1cb51..fc25290079a 100644
--- a/src/ansi-c/ansi_c_entry_point.cpp
+++ b/src/ansi-c/ansi_c_entry_point.cpp
@@ -18,6 +18,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/config.h>
 #include <util/cprover_prefix.h>
 #include <util/prefix.h>
+#include <util/symbol.h>
 
 #include <util/c_types.h>
 #include <ansi-c/string_constant.h>
@@ -120,7 +121,6 @@ void record_function_outputs(
 
 bool ansi_c_entry_point(
   symbol_tablet &symbol_table,
-  const std::string &standard_main,
   message_handlert &message_handler)
 {
   // check if entry point is already there
@@ -167,7 +167,7 @@ bool ansi_c_entry_point(
     main_symbol=matches.front();
   }
   else
-    main_symbol=standard_main;
+    main_symbol=ID_main;
 
   // look it up
   symbol_tablet::symbolst::const_iterator s_it=
@@ -190,6 +190,23 @@ bool ansi_c_entry_point(
   if(static_lifetime_init(symbol_table, symbol.location, message_handler))
     return true;
 
+  return generate_ansi_c_start_function(symbol, symbol_table, message_handler);
+}
+
+
+/// Generate a _start function for a specific function
+/// \param symbol: The symbol for the function that should be
+///   used as the entry point
+/// \param symbol_table: The symbol table for the program. The new _start
+///   function symbol will be added to this table
+/// \param message_handler: The message handler
+/// \return Returns false if the _start method was generated correctly
+bool generate_ansi_c_start_function(
+  const symbolt &symbol,
+  symbol_tablet &symbol_table,
+  message_handlert &message_handler)
+{
+  PRECONDITION(!symbol.value.is_nil());
   code_blockt init_code;
 
   // build call to initialization function
@@ -237,7 +254,7 @@ bool ansi_c_entry_point(
   const code_typet::parameterst &parameters=
     to_code_type(symbol.type).parameters();
 
-  if(symbol.name==standard_main)
+  if(symbol.name==ID_main)
   {
     if(parameters.empty())
     {
diff --git a/src/ansi-c/ansi_c_entry_point.h b/src/ansi-c/ansi_c_entry_point.h
index 835dd31845d..fe0ed04a2c1 100644
--- a/src/ansi-c/ansi_c_entry_point.h
+++ b/src/ansi-c/ansi_c_entry_point.h
@@ -15,7 +15,11 @@ Author: Daniel Kroening, kroening@kroening.com
 
 bool ansi_c_entry_point(
   symbol_tablet &symbol_table,
-  const std::string &standard_main,
+  message_handlert &message_handler);
+
+bool generate_ansi_c_start_function(
+  const symbolt &symbol,
+  symbol_tablet &symbol_table,
   message_handlert &message_handler);
 
 #endif // CPROVER_ANSI_C_ANSI_C_ENTRY_POINT_H
diff --git a/src/ansi-c/ansi_c_language.cpp b/src/ansi-c/ansi_c_language.cpp
index 46024683f96..19696264996 100644
--- a/src/ansi-c/ansi_c_language.cpp
+++ b/src/ansi-c/ansi_c_language.cpp
@@ -36,6 +36,22 @@ void ansi_c_languaget::modules_provided(std::set<std::string> &modules)
   modules.insert(get_base_name(parse_path, true));
 }
 
+/// Generate a _start function for a specific function
+/// \param entry_function_symbol_id: The symbol for the function that should be
+///   used as the entry point
+/// \param symbol_table: The symbol table for the program. The new _start
+///   function symbol will be added to this table
+/// \return Returns false if the _start method was generated correctly
+bool ansi_c_languaget::generate_start_function(
+  const irep_idt &entry_function_symbol_id,
+  symbol_tablet &symbol_table)
+{
+  return generate_ansi_c_start_function(
+    symbol_table.symbols.at(entry_function_symbol_id),
+    symbol_table,
+    *message_handler);
+}
+
 /// ANSI-C preprocessing
 bool ansi_c_languaget::preprocess(
   std::istream &instream,
@@ -127,8 +143,7 @@ bool ansi_c_languaget::typecheck(
 bool ansi_c_languaget::final(symbol_tablet &symbol_table)
 {
   generate_opaque_method_stubs(symbol_table);
-
-  if(ansi_c_entry_point(symbol_table, "main", get_message_handler()))
+  if(ansi_c_entry_point(symbol_table, get_message_handler()))
     return true;
 
   return false;
diff --git a/src/ansi-c/ansi_c_language.h b/src/ansi-c/ansi_c_language.h
index e20593c1f03..b86499954c2 100644
--- a/src/ansi-c/ansi_c_language.h
+++ b/src/ansi-c/ansi_c_language.h
@@ -73,6 +73,10 @@ class ansi_c_languaget:public languaget
 
   void modules_provided(std::set<std::string> &modules) override;
 
+  virtual bool generate_start_function(
+    const irep_idt &entry_function_symbol_id,
+    class symbol_tablet &symbol_table) override;
+
 protected:
   ansi_c_parse_treet parse_tree;
   std::string parse_path;
diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
index a3fbd8c99dc..265759fc698 100644
--- a/src/cbmc/cbmc_parse_options.cpp
+++ b/src/cbmc/cbmc_parse_options.cpp
@@ -51,6 +51,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <goto-programs/show_properties.h>
 #include <goto-programs/string_abstraction.h>
 #include <goto-programs/string_instrumentation.h>
+#include <goto-programs/rebuild_goto_start_function.h>
 
 #include <goto-symex/rewrite_union.h>
 #include <goto-symex/adjust_float_expressions.h>
@@ -624,8 +625,24 @@ int cbmc_parse_optionst::get_goto_program(
   try
   {
     if(initialize_goto_model(goto_model, cmdline, get_message_handler()))
+    // Remove all binaries from the command line as they
+    // are already compiled
       return 6;
 
+    if(cmdline.isset("function"))
+    {
+      const std::string &function_id=cmdline.get_value("function");
+      rebuild_goto_start_functiont start_function_rebuilder(
+        get_message_handler(),
+        goto_model.symbol_table,
+        goto_model.goto_functions);
+
+      if(start_function_rebuilder(function_id))
+      {
+        return 6;
+      }
+    }
+
     if(cmdline.isset("show-symbol-table"))
     {
       show_symbol_table(goto_model, ui_message_handler.get_ui());
@@ -992,7 +1009,7 @@ void cbmc_parse_optionst::help()
     " --round-to-plus-inf          rounding towards plus infinity\n"
     " --round-to-minus-inf         rounding towards minus infinity\n"
     " --round-to-zero              rounding towards zero\n"
-    " --function name              set main function name\n"
+    HELP_FUNCTIONS
     "\n"
     "Program representations:\n"
     " --show-parse-tree            show parse tree\n"
diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h
index e0d23a986c0..85461fef191 100644
--- a/src/cbmc/cbmc_parse_options.h
+++ b/src/cbmc/cbmc_parse_options.h
@@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/ui_message.h>
 #include <util/parse_options.h>
+#include <goto-programs/rebuild_goto_start_function.h>
 
 #include <analyses/goto_check.h>
 
@@ -26,7 +27,8 @@ class goto_functionst;
 class optionst;
 
 #define CBMC_OPTIONS \
-  "(program-only)(function):(preprocess)(slice-by-trace):" \
+  "(program-only)(preprocess)(slice-by-trace):" \
+  OPT_FUNCTIONS \
   "(no-simplify)(unwind):(unwindset):(slice-formula)(full-slice)" \
   "(debug-level):(no-propagation)(no-simplify-if)" \
   "(document-subgoals)(outfile):(test-preprocessor)" \
diff --git a/src/cpp/cpp_language.cpp b/src/cpp/cpp_language.cpp
index baa06dbcd48..f329e9986c0 100644
--- a/src/cpp/cpp_language.cpp
+++ b/src/cpp/cpp_language.cpp
@@ -53,6 +53,22 @@ void cpp_languaget::modules_provided(std::set<std::string> &modules)
   modules.insert(get_base_name(parse_path, true));
 }
 
+/// Generate a _start function for a specific function
+/// \param entry_function_symbol_id: The symbol for the function that should be
+///   used as the entry point
+/// \param symbol_table: The symbol table for the program. The new _start
+///   function symbol will be added to this table
+/// \return Returns false if the _start method was generated correctly
+bool cpp_languaget::generate_start_function(
+  const irep_idt &entry_function_symbol_id,
+  symbol_tablet &symbol_table)
+{
+  return generate_ansi_c_start_function(
+    symbol_table.lookup(entry_function_symbol_id),
+    symbol_table,
+    *message_handler);
+}
+
 /// ANSI-C preprocessing
 bool cpp_languaget::preprocess(
   std::istream &instream,
@@ -136,7 +152,7 @@ bool cpp_languaget::typecheck(
 
 bool cpp_languaget::final(symbol_tablet &symbol_table)
 {
-  if(ansi_c_entry_point(symbol_table, "main", get_message_handler()))
+  if(ansi_c_entry_point(symbol_table, get_message_handler()))
     return true;
 
   return false;
diff --git a/src/cpp/cpp_language.h b/src/cpp/cpp_language.h
index c43f9304a98..36093b8ba8a 100644
--- a/src/cpp/cpp_language.h
+++ b/src/cpp/cpp_language.h
@@ -85,6 +85,10 @@ class cpp_languaget:public languaget
 
   void modules_provided(std::set<std::string> &modules) override;
 
+  virtual bool generate_start_function(
+    const irep_idt &entry_function_symbol_id,
+    class symbol_tablet &symbol_table) override;
+
 protected:
   cpp_parse_treet cpp_parse_tree;
   std::string parse_path;
diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp
index b7f0b60a1d0..033dfddd025 100644
--- a/src/goto-analyzer/goto_analyzer_parse_options.cpp
+++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp
@@ -494,6 +494,7 @@ void goto_analyzer_parse_optionst::help()
     " --classpath dir/jar          set the classpath\n"
     " --main-class class-name      set the name of the main class\n"
     JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP
+    HELP_FUNCTIONS
     "\n"
     "Program representations:\n"
     " --show-parse-tree            show parse tree\n"
diff --git a/src/goto-analyzer/goto_analyzer_parse_options.h b/src/goto-analyzer/goto_analyzer_parse_options.h
index 3fbaab18b1b..62a5932cdb2 100644
--- a/src/goto-analyzer/goto_analyzer_parse_options.h
+++ b/src/goto-analyzer/goto_analyzer_parse_options.h
@@ -17,6 +17,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <goto-programs/goto_model.h>
 #include <goto-programs/show_goto_functions.h>
+#include <goto-programs/rebuild_goto_start_function.h>
 
 #include <analyses/goto_check.h>
 
@@ -27,7 +28,7 @@ class goto_functionst;
 class optionst;
 
 #define GOTO_ANALYSER_OPTIONS \
-  "(function):" \
+  OPT_FUNCTIONS \
   "D:I:(std89)(std99)(std11)" \
   "(classpath):(cp):(main-class):" \
   "(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \
diff --git a/src/goto-cc/compile.cpp b/src/goto-cc/compile.cpp
index 71f0d81160e..03cdd8544f6 100644
--- a/src/goto-cc/compile.cpp
+++ b/src/goto-cc/compile.cpp
@@ -368,7 +368,7 @@ bool compilet::link()
     symbol_table.remove(goto_functionst::entry_point());
     compiled_functions.function_map.erase(goto_functionst::entry_point());
 
-    if(ansi_c_entry_point(symbol_table, "main", get_message_handler()))
+    if(ansi_c_entry_point(symbol_table, get_message_handler()))
       return true;
 
     // entry_point may (should) add some more functions.
diff --git a/src/goto-programs/Makefile b/src/goto-programs/Makefile
index b164beef079..4da25537292 100644
--- a/src/goto-programs/Makefile
+++ b/src/goto-programs/Makefile
@@ -36,6 +36,7 @@ SRC = basic_blocks.cpp \
       property_checker.cpp \
       read_bin_goto_object.cpp \
       read_goto_binary.cpp \
+      rebuild_goto_start_function.cpp \
       remove_asm.cpp \
       remove_complex.cpp \
       remove_const_function_pointers.cpp \
diff --git a/src/goto-programs/initialize_goto_model.cpp b/src/goto-programs/initialize_goto_model.cpp
index 1706643206f..753dff36edb 100644
--- a/src/goto-programs/initialize_goto_model.cpp
+++ b/src/goto-programs/initialize_goto_model.cpp
@@ -21,6 +21,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <langapi/mode.h>
 #include <langapi/language_ui.h>
 
+#include <goto-programs/rebuild_goto_start_function.h>
+
 #include "goto_convert_functions.h"
 #include "read_goto_binary.h"
 
@@ -131,6 +133,20 @@ bool initialize_goto_model(
         return true;
     }
 
+    if(cmdline.isset("function"))
+    {
+      const std::string &function_id=cmdline.get_value("function");
+      rebuild_goto_start_functiont start_function_rebuilder(
+        msg.get_message_handler(),
+        goto_model.symbol_table,
+        goto_model.goto_functions);
+
+      if(start_function_rebuilder(function_id))
+      {
+        return 6;
+      }
+    }
+
     msg.status() << "Generating GOTO Program" << messaget::eom;
 
     goto_convert(
diff --git a/src/goto-programs/rebuild_goto_start_function.cpp b/src/goto-programs/rebuild_goto_start_function.cpp
new file mode 100644
index 00000000000..0949c1da73f
--- /dev/null
+++ b/src/goto-programs/rebuild_goto_start_function.cpp
@@ -0,0 +1,109 @@
+/*******************************************************************\
+ Module: Goto Programs
+ Author: Thomas Kiley, thomas@diffblue.com
+\*******************************************************************/
+
+/// \file
+/// Goto Programs Author: Thomas Kiley, thomas@diffblue.com
+
+#include "rebuild_goto_start_function.h"
+
+#include <goto-programs/goto_functions.h>
+#include <util/language.h>
+#include <util/symbol.h>
+#include <util/symbol_table.h>
+#include <util/prefix.h>
+#include <langapi/mode.h>
+#include <memory>
+
+/// To rebuild the _start funciton in the event the program was compiled into
+/// GOTO with a different entry function selected.
+/// \param _message_handler: The message handler to report any messages with
+/// \param symbol_table: The symbol table of the program (to replace the _start
+///   functions symbo)
+/// \param goto_functions: The goto functions of the program (to replace the
+///   body of the _start function).
+rebuild_goto_start_functiont::rebuild_goto_start_functiont(
+  message_handlert &_message_handler,
+  symbol_tablet &symbol_table,
+  goto_functionst &goto_functions):
+  messaget(_message_handler),
+  symbol_table(symbol_table),
+  goto_functions(goto_functions)
+{
+}
+
+/// To rebuild the _start function in the event the program was compiled into
+/// GOTO with a different entry function selected. It works by discarding the
+/// _start symbol and GOTO function and calling on the relevant languaget to
+/// generate the _start function again.
+/// \param entry_function: The name of the entry function that should be
+/// called from _start
+/// \return Returns true if either the symbol is not found, or something went
+///   wrong with generating the start_function. False otherwise.
+bool rebuild_goto_start_functiont::operator()(
+  const irep_idt &entry_function)
+{
+  const irep_idt &mode=get_entry_point_mode();
+
+  // Get the relevant languaget to generate the new entry point with
+  std::unique_ptr<languaget> language=get_language_from_mode(mode);
+  INVARIANT(language, "No language found for mode: "+id2string(mode));
+  language->set_message_handler(get_message_handler());
+
+  // To create a new entry point we must first remove the old one
+  remove_existing_entry_point();
+
+  bool return_code=
+    language->generate_start_function(entry_function, symbol_table);
+
+  // Remove the function from the goto_functions so it is copied back in
+  // from the symbol table during goto_convert
+  if(!return_code)
+  {
+    const auto &start_function=
+      goto_functions.function_map.find(goto_functionst::entry_point());
+    if(start_function!=goto_functions.function_map.end())
+    {
+      goto_functions.function_map.erase(start_function);
+    }
+  }
+
+  return return_code;
+}
+
+/// Find out the mode of the current entry point to determine the mode of the
+/// replacement entry point
+/// \return A mode string saying which language to use
+irep_idt rebuild_goto_start_functiont::get_entry_point_mode() const
+{
+  const symbolt &current_entry_point=
+    symbol_table.lookup(goto_functionst::entry_point());
+  return current_entry_point.mode;
+}
+
+/// Eliminate the existing entry point function symbol and any symbols created
+/// in that scope from the symbol table.
+void rebuild_goto_start_functiont::remove_existing_entry_point()
+{
+  // Remove the function itself
+  symbol_table.remove(goto_functionst::entry_point());
+
+  // And any symbols created in the scope of the entry point
+  std::vector<irep_idt> entry_point_symbols;
+  for(const auto &symbol_entry : symbol_table.symbols)
+  {
+    const bool is_entry_point_symbol=
+      has_prefix(
+        id2string(symbol_entry.first),
+        id2string(goto_functionst::entry_point()));
+
+    if(is_entry_point_symbol)
+      entry_point_symbols.push_back(symbol_entry.first);
+  }
+
+  for(const irep_idt &entry_point_symbol : entry_point_symbols)
+  {
+    symbol_table.remove(entry_point_symbol);
+  }
+}
diff --git a/src/goto-programs/rebuild_goto_start_function.h b/src/goto-programs/rebuild_goto_start_function.h
new file mode 100644
index 00000000000..870e05a61f6
--- /dev/null
+++ b/src/goto-programs/rebuild_goto_start_function.h
@@ -0,0 +1,42 @@
+/*******************************************************************\
+ Module: Goto Programs
+ Author: Thomas Kiley, thomas@diffblue.com
+\*******************************************************************/
+
+/// \file
+/// Goto Programs Author: Thomas Kiley, thomas@diffblue.com
+
+#ifndef CPROVER_GOTO_PROGRAMS_REBUILD_GOTO_START_FUNCTION_H
+#define CPROVER_GOTO_PROGRAMS_REBUILD_GOTO_START_FUNCTION_H
+
+#include <util/message.h>
+
+class symbol_tablet;
+class goto_functionst;
+
+#define OPT_FUNCTIONS \
+  "(function):"
+
+#define HELP_FUNCTIONS \
+  " --function name              set main function name\n"
+
+class rebuild_goto_start_functiont: public messaget
+{
+public:
+  rebuild_goto_start_functiont(
+    message_handlert &_message_handler,
+    symbol_tablet &symbol_table,
+    goto_functionst &goto_functions);
+
+  bool operator()(const irep_idt &entry_function);
+
+private:
+  irep_idt get_entry_point_mode() const;
+
+  void remove_existing_entry_point();
+
+  symbol_tablet &symbol_table;
+  goto_functionst &goto_functions;
+};
+
+#endif // CPROVER_GOTO_PROGRAMS_REBUILD_GOTO_START_FUNCTION_H
diff --git a/src/java_bytecode/java_bytecode_language.cpp b/src/java_bytecode/java_bytecode_language.cpp
index 7711940b781..8ea79aafa6d 100644
--- a/src/java_bytecode/java_bytecode_language.cpp
+++ b/src/java_bytecode/java_bytecode_language.cpp
@@ -106,6 +106,30 @@ void java_bytecode_languaget::modules_provided(std::set<std::string> &modules)
   // modules.insert(translation_unit(parse_path));
 }
 
+/// Generate a _start function for a specific function.
+/// \param entry_function_symbol_id: The symbol for the function that should be
+///   used as the entry point
+/// \param symbol_table: The symbol table for the program. The new _start
+///   function symbol will be added to this table
+/// \return Returns false if the _start method was generated correctly
+bool java_bytecode_languaget::generate_start_function(
+  const irep_idt &entry_function_symbol_id,
+  symbol_tablet &symbol_table)
+{
+  const auto res=
+    get_main_symbol(
+      symbol_table, entry_function_symbol_id, get_message_handler());
+
+  return generate_java_start_function(
+    res.main_function,
+    symbol_table,
+    get_message_handler(),
+    assume_inputs_non_null,
+    max_nondet_array_length,
+    max_nondet_tree_depth,
+    *pointer_type_selector);
+}
+
 /// ANSI-C preprocessing
 bool java_bytecode_languaget::preprocess(
   std::istream &instream,
diff --git a/src/java_bytecode/java_bytecode_language.h b/src/java_bytecode/java_bytecode_language.h
index c70e7ce082a..21cacce6465 100644
--- a/src/java_bytecode/java_bytecode_language.h
+++ b/src/java_bytecode/java_bytecode_language.h
@@ -137,6 +137,10 @@ class java_bytecode_languaget:public languaget
   virtual void convert_lazy_method(
     const irep_idt &id, symbol_tablet &) override;
 
+  virtual bool generate_start_function(
+    const irep_idt &entry_function_symbol_id,
+    class symbol_tablet &symbol_table) override;
+
 protected:
   bool do_ci_lazy_method_conversion(symbol_tablet &, lazy_methodst &);
   const select_pointer_typet &get_pointer_type_selector() const;
diff --git a/src/java_bytecode/java_entry_point.cpp b/src/java_bytecode/java_entry_point.cpp
index c142f37ddf5..12e806b8e2f 100644
--- a/src/java_bytecode/java_entry_point.cpp
+++ b/src/java_bytecode/java_entry_point.cpp
@@ -510,6 +510,39 @@ bool java_entry_point(
     max_nondet_tree_depth,
     pointer_type_selector);
 
+  return generate_java_start_function(
+    symbol,
+    symbol_table,
+    message_handler,
+    assume_init_pointers_not_null,
+    max_nondet_array_length,
+    max_nondet_tree_depth,
+    pointer_type_selector);
+}
+
+/// Generate a _start function for a specific function. See
+/// java_entry_point for more details.
+/// \param symbol: The symbol representing the function to call
+/// \param symbol_table: Global symbol table
+/// \param message_handler: Where to write output to
+/// \param assume_init_pointers_not_null: When creating pointers, assume they
+///   always take a non-null value.
+/// \param max_nondet_array_length: The length of the arrays to create when
+///   filling them
+/// \param max_nondet_tree_depth: defines the maximum depth of the object tree
+///   (see java_entry_points documentation for details)
+/// \param pointer_type_selector: Logic for substituting types of pointers
+/// \returns true if error occurred on entry point search, false otherwise
+bool generate_java_start_function(
+  const symbolt &symbol,
+  symbol_tablet &symbol_table,
+  message_handlert &message_handler,
+  bool assume_init_pointers_not_null,
+  size_t max_nondet_array_length,
+  size_t max_nondet_tree_depth,
+  const select_pointer_typet &pointer_type_selector)
+{
+  messaget message(message_handler);
   code_blockt init_code;
 
   // build call to initialization function
diff --git a/src/java_bytecode/java_entry_point.h b/src/java_bytecode/java_entry_point.h
index 18e42aafc65..cc03e8480b5 100644
--- a/src/java_bytecode/java_entry_point.h
+++ b/src/java_bytecode/java_entry_point.h
@@ -40,4 +40,13 @@ main_function_resultt get_main_symbol(
   message_handlert &,
   bool allow_no_body=false);
 
+bool generate_java_start_function(
+  const symbolt &symbol,
+  class symbol_tablet &symbol_table,
+  class message_handlert &message_handler,
+  bool assume_init_pointers_not_null,
+  size_t max_nondet_array_length,
+  size_t max_nondet_tree_depth,
+  const select_pointer_typet &pointer_type_selector);
+
 #endif // CPROVER_JAVA_BYTECODE_JAVA_ENTRY_POINT_H
diff --git a/src/jsil/jsil_language.cpp b/src/jsil/jsil_language.cpp
index f0c5ad38c13..94f16cc5cb8 100644
--- a/src/jsil/jsil_language.cpp
+++ b/src/jsil/jsil_language.cpp
@@ -41,6 +41,22 @@ bool jsil_languaget::interfaces(symbol_tablet &symbol_table)
   return false;
 }
 
+/// Generate a _start function for a specific function
+/// \param entry_function_symbol_id: The symbol for the function that should be
+///   used as the entry point
+/// \param symbol_table: The symbol table for the program. The new _start
+///   function symbol will be added to this table
+/// \return Returns false if the _start method was generated correctly
+bool jsil_languaget::generate_start_function(
+  const irep_idt &entry_function_symbol_id,
+  symbol_tablet &symbol_table)
+{
+  // TODO(tkiley): This should be implemented if this language
+  // is used.
+  UNREACHABLE;
+  return true;
+}
+
 bool jsil_languaget::preprocess(
   std::istream &instream,
   const std::string &path,
diff --git a/src/jsil/jsil_language.h b/src/jsil/jsil_language.h
index da889e111a1..6ff0c852bdb 100644
--- a/src/jsil/jsil_language.h
+++ b/src/jsil/jsil_language.h
@@ -25,19 +25,19 @@ class jsil_languaget:public languaget
   virtual bool preprocess(
     std::istream &instream,
     const std::string &path,
-    std::ostream &outstream);
+    std::ostream &outstream) override;
 
   virtual bool parse(
     std::istream &instream,
-    const std::string &path);
+    const std::string &path) override;
 
   virtual bool typecheck(
     symbol_tablet &context,
-    const std::string &module);
+    const std::string &module) override;
 
-  virtual bool final(symbol_tablet &context);
+  virtual bool final(symbol_tablet &context) override;
 
-  virtual void show_parse(std::ostream &out);
+  virtual void show_parse(std::ostream &out) override;
 
   virtual ~jsil_languaget();
   jsil_languaget() { }
@@ -45,29 +45,33 @@ class jsil_languaget:public languaget
   virtual bool from_expr(
     const exprt &expr,
     std::string &code,
-    const namespacet &ns);
+    const namespacet &ns) override;
 
   virtual bool from_type(
     const typet &type,
     std::string &code,
-    const namespacet &ns);
+    const namespacet &ns) override;
 
   virtual bool to_expr(
     const std::string &code,
     const std::string &module,
     exprt &expr,
-    const namespacet &ns);
+    const namespacet &ns) override;
 
-  virtual std::unique_ptr<languaget> new_language()
+  virtual std::unique_ptr<languaget> new_language() override
   { return util_make_unique<jsil_languaget>(); }
 
-  virtual std::string id() const { return "jsil"; }
-  virtual std::string description() const
+  virtual std::string id() const override { return "jsil"; }
+  virtual std::string description() const override
   { return "Javascript Intermediate Language"; }
-  virtual std::set<std::string> extensions() const;
+  virtual std::set<std::string> extensions() const override;
 
-  virtual void modules_provided(std::set<std::string> &modules);
-  virtual bool interfaces(symbol_tablet &symbol_table);
+  virtual void modules_provided(std::set<std::string> &modules) override;
+  virtual bool interfaces(symbol_tablet &symbol_table) override;
+
+  virtual bool generate_start_function(
+    const irep_idt &entry_function_symbol_id,
+    class symbol_tablet &symbol_table) override;
 
 protected:
   jsil_parse_treet parse_tree;
diff --git a/src/symex/symex_parse_options.cpp b/src/symex/symex_parse_options.cpp
index 5d96f2d5949..e85a369340e 100644
--- a/src/symex/symex_parse_options.cpp
+++ b/src/symex/symex_parse_options.cpp
@@ -587,7 +587,7 @@ void symex_parse_optionst::help()
     " --round-to-plus-inf          IEEE floating point rounding mode\n"
     " --round-to-minus-inf         IEEE floating point rounding mode\n"
     " --round-to-zero              IEEE floating point rounding mode\n"
-    " --function name              set main function name\n"
+    HELP_FUNCTIONS
     "\n"
     "Java Bytecode frontend options:\n"
     JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP
diff --git a/src/symex/symex_parse_options.h b/src/symex/symex_parse_options.h
index a3fb841f20b..c2aec7a175b 100644
--- a/src/symex/symex_parse_options.h
+++ b/src/symex/symex_parse_options.h
@@ -17,6 +17,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <goto-programs/goto_model.h>
 #include <goto-programs/show_goto_functions.h>
+#include <goto-programs/rebuild_goto_start_function.h>
 
 #include <analyses/goto_check.h>
 
@@ -28,7 +29,7 @@ class goto_functionst;
 class optionst;
 
 #define SYMEX_OPTIONS \
-  "(function):" \
+  OPT_FUNCTIONS \
   "D:I:" \
   "(depth):(context-bound):(branch-bound):(unwind):(max-search-time):" \
   OPT_GOTO_CHECK \
diff --git a/src/util/language.h b/src/util/language.h
index ebe10bba1a8..d3b25165c3b 100644
--- a/src/util/language.h
+++ b/src/util/language.h
@@ -119,6 +119,10 @@ class languaget:public messaget
 
   void set_should_generate_opaque_method_stubs(bool should_generate_stubs);
 
+  virtual bool generate_start_function(
+    const irep_idt &entry_function_symbol_id,
+    class symbol_tablet &symbol_table)=0;
+
   // constructor / destructor
 
   languaget() { }