Skip to content

Commit a0fe71a

Browse files
authored
Merge pull request #5834 from tautschnig/fix-generate_ansi_c_start_function
generate_ansi_c_start_function reports user errors via return code
2 parents fd53863 + 2c59e0d commit a0fe71a

File tree

3 files changed

+14
-10
lines changed

3 files changed

+14
-10
lines changed

regression/cbmc/human-readable-error-on-wrong-main-signature/test.desc renamed to regression/ansi-c/human-readable-error-on-wrong-main-signature/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@ CORE
22
main.c
33

44
'main' with signature .* found
5-
^EXIT=6$
5+
^EXIT=(1|64)$
66
^SIGNAL=0$
77
--
88
Invariant check failed

src/ansi-c/ansi_c_entry_point.cpp

+13-9
Original file line numberDiff line numberDiff line change
@@ -478,15 +478,19 @@ bool generate_ansi_c_start_function(
478478
{
479479
const namespacet ns{symbol_table};
480480
const std::string main_signature = type2c(symbol.type, ns);
481-
throw invalid_source_file_exceptiont{
482-
"'main' with signature '" + main_signature +
483-
"' found,"
484-
" but expecting one of:\n"
485-
" int main(void)\n"
486-
" int main(int argc, char *argv[])\n"
487-
" int main(int argc, char *argv[], char *envp[])\n"
488-
"If this is a non-standard main entry point please provide a custom\n"
489-
"entry function and point to it via cbmc --function instead"};
481+
messaget message(message_handler);
482+
message.error().source_location = symbol.location;
483+
message.error() << "'main' with signature '" << main_signature
484+
<< "' found,"
485+
<< " but expecting one of:\n"
486+
<< " int main(void)\n"
487+
<< " int main(int argc, char *argv[])\n"
488+
<< " int main(int argc, char *argv[], char *envp[])\n"
489+
<< "If this is a non-standard main entry point please "
490+
"provide a custom\n"
491+
<< "entry function and use --function instead"
492+
<< messaget::eom;
493+
return true;
490494
}
491495
}
492496
else

0 commit comments

Comments
 (0)