Skip to content
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.

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

goto-instrument --remove-function-body #730

Merged
merged 1 commit into from
May 25, 2017

Conversation

tautschnig
Copy link
Collaborator

No description provided.

@tautschnig tautschnig changed the title Utility analyses to inspect functions (and function calls) in goto binaries goto-instrument --remove-function-body Apr 10, 2017
@tautschnig tautschnig force-pushed the inspect-functions branch from e3f281d to 14875e9 Compare May 12, 2017 14:07
Copy link
Contributor

@thk123 thk123 left a comment

Choose a reason for hiding this comment

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

Just a couple of things that look a little odd to me.

@@ -1637,6 +1647,7 @@ void goto_instrument_parse_optionst::help()
HELP_REMOVE_CONST_FUNCTION_POINTERS
" --add-library add models of C library functions\n"
" --model-argc-argv <n> model up to <n> command line arguments\n"
" --remove-function-body <f> remove the implementation of function <f>\n"
Copy link
Contributor

Choose a reason for hiding this comment

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

Per the coding standard, it would be good if this flag could be moved to the code that implements it, unless this really can only be used in goto-instrument?

Copy link
Contributor

Choose a reason for hiding this comment

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

Could it also be clearer that here you can provide multiple fs to remove multiple functions.

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

Will fix (but just the latter; this function is really for goto-instrument only).


Outputs:

Purpose:
Copy link
Contributor

Choose a reason for hiding this comment

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

Missing documentation

--remove-function-body foo --remove-function-body bar
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
Copy link
Contributor

Choose a reason for hiding this comment

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

I appreciate that it is hard to actually test anything from the output, but it might be good if we could run --show-goto-functions on the output and check that bar is really removed?

Alternatively, if you grab #874, it might be relatively easy to add some unit tests for this.

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

I have added patterns that must not be found in test.desc, so I think this is addressed.


Author: Michael Tautschnig

Date: April 2017
Copy link
Contributor

Choose a reason for hiding this comment

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

This comment block doesn't normally have the date, how come we've added it here?

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

$ git grep ^Date: | wc -l
     152

Seems it's all very much inconsistent.


#include <goto-programs/goto_functions.h>

#include "remove_function.h"
Copy link
Contributor

Choose a reason for hiding this comment

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

Per #890 this should be the first include

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

Ack.

@tautschnig tautschnig force-pushed the inspect-functions branch from 14875e9 to 50d3563 Compare May 22, 2017 11:14
Removes the implementation of a function (but not its declaration or its call
sites) from a goto program. This enables stubbing of possibly costly functions,
such as custom memset implementations.
@tautschnig tautschnig force-pushed the inspect-functions branch from 50d3563 to accc412 Compare May 22, 2017 11:16
@kroening kroening merged commit be0ded1 into diffblue:master May 25, 2017
@tautschnig tautschnig deleted the inspect-functions branch May 25, 2017 18:54
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants