Merge pull request #5416 from hannes-steffenhagen-diffblue/fix/human-…

…readable-error-on-wrong-main-signature

Add human readable error message for invalid main signatures

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)
+{
+}

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

src/ansi-c/ansi_c_entry_point.cpp

@@ -18,6 +18,7 @@ Author: Daniel Kroening, [email protected]
 #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
   {