Add human readable error message for invalid main signatures #5416
Conversation
Currently we have special handling if the entry point for analysis is called
`main`, in particular we assume it is one of the following:
int main(void)
int main(int argc, char *argv[])
int main(int argc, char *argv[], char *envp[])
If it is not so far we have been failing with an UNREACHABLE invariant failure.
Since it is completely possible to have a main signature like that, we should
fail with a proper human readable error message that tells people what is wrong
and maybe how they can work around it.
hannes-steffenhagen-diffblue
requested review from
chrisr-diffblue,
kroening and
tautschnig
as code owners
|
Is there a long term plan for better handling of the situation? Or is it how we're going to work with this? |
|
@NlightNFotis Like I said, I am not sure what the ‘better’ version looks like. |
Codecov Report
@@ Coverage Diff @@
## develop #5416 +/- ##
========================================
Coverage 68.20% 68.21%
========================================
Files 1176 1176
Lines 97521 97524 +3
========================================
+ Hits 66518 66522 +4
+ Misses 31003 31002 -1
Continue to review full report at Codecov.
|
| " 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"}; |
There was a problem hiding this comment.
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
There was a problem hiding this comment.
It doesn’t unfortunately. What does work is adding something like
void harness(void) {
main(NULL);
}
and pointing at that.
| const namespacet ns{symbol_table}; | ||
| const std::string main_signature = type2c(symbol.type, ns); | ||
| throw invalid_source_file_exceptiont{ | ||
| "'main' with signature '" + main_signature + |
There was a problem hiding this comment.
Should it explicitly say "with an invalid signature" ?
There was a problem hiding this comment.
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.
| " 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" |
There was a problem hiding this comment.
Thanks for the extra user help in the message :-)
hannes-steffenhagen-diffblue
deleted the
fix/human-readable-error-on-wrong-main-signature
branch
Currently we have special handling if the entry point for analysis is called
main, in particular we assume it is one of the following:If it is not so far we have been failing with an UNREACHABLE invariant failure.
Since it is completely possible to have a main signature like that, we should
fail with a proper human readable error message that tells people what is wrong
and maybe how they can work around it.
For now, addresses #5415. As I say in that ticket maybe we want to handle non-standard
mainsignatures in a more graceful way, but until we decide on that having a better error message should take away some of the pain.