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 +#include + +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 #include "c_nondet_symbol_factory.h" +#include "expr2c.h" exprt::operandst build_function_environment( const code_typet::parameterst ¶meters, @@ -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 {