Added a warning for when function returns a value but has return void #301
Conversation
|
@cristina-david I think I should assign this to you, but I can't work out how to change the assignee. I suppose it is a permissions thing? For context, I thought I'd got stuck trying to get the interpreter to give me the return variable, but actually I was being silly and had the return type as void. When Chris spotted this after I asked for help, he suggested I added a warning to the C to GOTO compiler to catch this mistake. |
| { | ||
| warning() << "Function " << code.source_location().get_function(); | ||
| warning() << " has return void but a return statement returning "; | ||
| warning() << follow(code.op0().type()).id(); |
There was a problem hiding this comment.
Use to_string here, to print the usual ANSI-C syntax
| warning() << "Function " << code.source_location().get_function(); | ||
| warning() << " has return void but a return statement returning "; | ||
| warning() << follow(code.op0().type()).id(); | ||
| warning() << " was found on line " << code.source_location().get_line(); |
There was a problem hiding this comment.
Use warning().set_source_location instead.
| @@ -911,7 +911,15 @@ void c_typecheck_baset::typecheck_return(codet &code) | |||
| { | |||
| // gcc doesn't actually complain, it just warns! | |||
| if(follow(code.op0().type()).id()!=ID_empty) | |||
| { | |||
| warning().source_location = code.source_location(); | |||
There was a problem hiding this comment.
nit picking: don't put spaces around assignment operator
| CORE | ||
| main.c | ||
| --verbosity 2 | ||
| ^file main.c line . function fun: Function has return void but a return statement returning signed int$ |
There was a problem hiding this comment.
I would suggest to insist the warning checks specifically for line 3
| { | ||
| warning().source_location = code.source_location(); | ||
|
|
||
| warning() << "Function has return void but a return statement returning "; |
There was a problem hiding this comment.
We seem to be starting all warnings with a lowercase character (i.e., use "function")
Also, that line is rather long, consider breaking it earlier.
|
@thk123 Many thanks for carefully addressing all the feedback! It might be best to now squash all three commits into one. |
|
@tautschnig You are right, I mentioned an internal issue |
|
This seems ready to get merged once it's squashed. |
Also included a simple regression that should produce this warning Set the source location on the warning and use the ANSI C version of the type. Also updated regression to reflect new format.
thk123
force-pushed
the
void-return-warning
branch
from
c82abe1 to
f28f7ac
Compare
…-clang-format Add symlink to .clang-format in cbmc folder
Also included a simple regression that should produce this warning