Skip to content

Add human readable error message for invalid main signatures #5416

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Jul 9, 2020
Merged

Add human readable error message for invalid main signatures #5416

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 12 additions & 0 deletions regression/cbmc/human-readable-error-on-wrong-main-signature/main.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
#include <assert.h>
#include <stddef.h>

struct foo
{
int x;
int y;
};

int main(struct foo *p)
{
}
11 changes: 11 additions & 0 deletions regression/cbmc/human-readable-error-on-wrong-main-signature/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
15 changes: 14 additions & 1 deletion src/ansi-c/ansi_c_entry_point.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down Expand Up @@ -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 +
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Should it explicitly say "with an invalid signature" ?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Well, I feel like ‘invalid’ is a matter of opinion. Maybe this is coming from code that does have a non-standard entry point. It is certainly not what we expect though, so saying that much is value neutral.

"' 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"
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks for the extra user help in the message :-)

"entry function and point to it via cbmc --function instead"};
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is a great error message 💚
❔ If I do cbmc main.c --function main does this work? No worries if not, but if it does, I'd be half tempted to give that as the advice

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It doesn’t unfortunately. What does work is adding something like

void harness(void) {
  main(NULL);
}

and pointing at that.

}
}
else
{
Expand Down