Skip to content

C entry point generator: no unconditional conversion to pointer type #6976

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
Sep 28, 2022
Merged

C entry point generator: no unconditional conversion to pointer type #6976

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
4 changes: 4 additions & 0 deletions regression/ansi-c/main1/main.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
int main(char *argv, int arc)
{
return 0;
}
11 changes: 11 additions & 0 deletions regression/ansi-c/main1/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
CORE test-c++-front-end
main.c

'main' with signature 'signed int \(char \*argv, signed int arc\)' found
^EXIT=(64|1)$
^SIGNAL=0$
--
Invariant check failed
Copy link

Choose a reason for hiding this comment

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

Can we add a description of what the test is trying to achieve? Maybe something like:

In this test, we detect a non-standard C entry point and gracefully exit with a message to the user.

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

Thank you, done!

--
This test is to ensure that non-standard C entry points are handled gracefully
and with a message to the user.
11 changes: 10 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 @@ -248,7 +248,16 @@ bool generate_ansi_c_start_function(
{
// ok
}
else if(parameters.size()==2 || parameters.size()==3)
// The C standard (and any related architecture descriptions) enforces an
// order of parameters. The user, however, may supply arbitrary
// (syntactically valid) C code, even one that does not respect the calling
// conventions set out in the C standard. If the user does supply such code,
// then we can only tell them that they got it wrong, which is what we do
// via the error message in the else branch of this code.
else if(
parameters.size() >= 2 && parameters[1].type().id() == ID_pointer &&
Copy link
Member

Choose a reason for hiding this comment

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

Did you mean parameters[0]?

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

No, parameters[0] is what we'd expect to be argc if I' not mistaken?

Copy link
Contributor

Choose a reason for hiding this comment

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

This looks wrong because the regression test has (char *argv, int argc) but the CBMC code is expecting/assuming the parameters in the other order. Is there a place where the code rewrites/forces the order, or is this actually entirely up to the code being sent to CBMC? If the former, a comment would clarify this, if the latter, then this code makes assumptions that may be wrong.

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

The one place that enforces the order is the C standard (and any related architecture descriptions). The user, however, may supply arbitrary (syntactically valid) C code, even one that does not respect the calling conventions set out in the C standard. If the user does supply such code (as is done in the accompanying regression test), then we can only tell them that they got it wrong, which is what we do via the error message in the else branch of this code. The change being proposed here should make sure that we do end up in this else branch.

Does this address your concern? Should I still be making changes to the implementation? Should I perhaps add the above as a comment?

Copy link
Contributor

Choose a reason for hiding this comment

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

Yes, I'm happy to approve. The detail in your response might be nice to have in the comments though since this is not immediately clear.

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

Comment added to the code.

Copy link

Choose a reason for hiding this comment

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

The comment is very helpful.

(parameters.size() == 2 ||
(parameters.size() == 3 && parameters[2].type().id() == ID_pointer)))
{
namespacet ns(symbol_table);

Expand Down