Skip to content

Commit 2c59e0d

Browse files
committed
generate_ansi_c_start_function reports user errors via return code
Do not throw an exception upon invalid source input. Instead, print an error message and return `true`.
1 parent d0c403a commit 2c59e0d

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
@@ -480,15 +480,19 @@ bool generate_ansi_c_start_function(
480480
{
481481
const namespacet ns{symbol_table};
482482
const std::string main_signature = type2c(symbol.type, ns);
483-
throw invalid_source_file_exceptiont{
484-
"'main' with signature '" + main_signature +
485-
"' found,"
486-
" but expecting one of:\n"
487-
" int main(void)\n"
488-
" int main(int argc, char *argv[])\n"
489-
" int main(int argc, char *argv[], char *envp[])\n"
490-
"If this is a non-standard main entry point please provide a custom\n"
491-
"entry function and point to it via cbmc --function instead"};
483+
messaget message(message_handler);
484+
message.error().source_location = symbol.location;
485+
message.error() << "'main' with signature '" << main_signature
486+
<< "' found,"
487+
<< " but expecting one of:\n"
488+
<< " int main(void)\n"
489+
<< " int main(int argc, char *argv[])\n"
490+
<< " int main(int argc, char *argv[], char *envp[])\n"
491+
<< "If this is a non-standard main entry point please "
492+
"provide a custom\n"
493+
<< "entry function and use --function instead"
494+
<< messaget::eom;
495+
return true;
492496
}
493497
}
494498
else

0 commit comments

Comments
 (0)