From 3b9b15577625c1694091497e074d695863d749cd Mon Sep 17 00:00:00 2001
From: Hannes Steffenhagen <hannes.steffenhagen@diffblue.com>
Date: Thu, 9 Jul 2020 11:32:36 +0100
Subject: [PATCH] Add human readable error message for invalid main signatures

Currently we have special handling if the entry point for analysis is called
`main`, in particular we assume it is one of the following:

    int main(void)
    int main(int argc, char *argv[])
    int main(int argc, char *argv[], char *envp[])

If it is not so far we have been failing with an UNREACHABLE invariant failure.
Since it is completely possible to have a main signature like that, we should
fail with a proper human readable error message that tells people what is wrong
and maybe how they can work around it.
---
 .../main.c                                        | 12 ++++++++++++
 .../test.desc                                     | 11 +++++++++++
 src/ansi-c/ansi_c_entry_point.cpp                 | 15 ++++++++++++++-
 3 files changed, 37 insertions(+), 1 deletion(-)
 create mode 100644 regression/cbmc/human-readable-error-on-wrong-main-signature/main.c
 create mode 100644 regression/cbmc/human-readable-error-on-wrong-main-signature/test.desc

diff --git a/regression/cbmc/human-readable-error-on-wrong-main-signature/main.c b/regression/cbmc/human-readable-error-on-wrong-main-signature/main.c
new file mode 100644
index 00000000000..0c9b63ab59e
--- /dev/null
+++ b/regression/cbmc/human-readable-error-on-wrong-main-signature/main.c
@@ -0,0 +1,12 @@
+#include <assert.h>
+#include <stddef.h>
+
+struct foo
+{
+  int x;
+  int y;
+};
+
+int main(struct foo *p)
+{
+}
diff --git a/regression/cbmc/human-readable-error-on-wrong-main-signature/test.desc b/regression/cbmc/human-readable-error-on-wrong-main-signature/test.desc
new file mode 100644
index 00000000000..10f03822c62
--- /dev/null
+++ b/regression/cbmc/human-readable-error-on-wrong-main-signature/test.desc
@@ -0,0 +1,11 @@
+CORE
+main.c
+
+'main' with signature .* found
+^EXIT=6$
+^SIGNAL=0$
+--
+Invariant check failed
+--
+This is just to check that CBMC doesn’t crash when we see a ‘main’ function
+with an unexpected signature, see https://github.com/diffblue/cbmc/issues/5415
diff --git a/src/ansi-c/ansi_c_entry_point.cpp b/src/ansi-c/ansi_c_entry_point.cpp
index d51e49d39d9..f4e462692e5 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 <linking/static_lifetime_init.h>
 
 #include "c_nondet_symbol_factory.h"
+#include "expr2c.h"
 
 exprt::operandst build_function_environment(
   const code_typet::parameterst &parameters,
@@ -473,7 +474,19 @@ bool generate_ansi_c_start_function(
       }
     }
     else
-      UNREACHABLE;
+    {
+      const namespacet ns{symbol_table};
+      const std::string main_signature = type2c(symbol.type, ns);
+      throw invalid_source_file_exceptiont{
+        "'main' with signature '" + main_signature +
+        "' found,"
+        " but expecting one of:\n"
+        "   int main(void)\n"
+        "   int main(int argc, char *argv[])\n"
+        "   int main(int argc, char *argv[], char *envp[])\n"
+        "If this is a non-standard main entry point please provide a custom\n"
+        "entry function and point to it via cbmc --function instead"};
+    }
   }
   else
   {