goto-instrument --remove-function-body #730
Conversation
tautschnig
force-pushed
the
inspect-functions
branch
from
bef294d to
97f0879
Compare
tautschnig
force-pushed
the
inspect-functions
branch
from
97f0879 to
b190685
Compare
tautschnig
changed the title
tautschnig
force-pushed
the
inspect-functions
branch
from
b190685 to
e3f281d
Compare
tautschnig
force-pushed
the
inspect-functions
branch
from
e3f281d to
14875e9
Compare
thk123
left a comment
thk123
left a comment
There was a problem hiding this comment.
Just a couple of things that look a little odd to me.
| 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" |
There was a problem hiding this comment.
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?
There was a problem hiding this comment.
Could it also be clearer that here you can provide multiple fs to remove multiple functions.
There was a problem hiding this comment.
Will fix (but just the latter; this function is really for goto-instrument only).
| Outputs: | ||
| Purpose: |
| --remove-function-body foo --remove-function-body bar | ||
| ^EXIT=0$ | ||
| ^SIGNAL=0$ | ||
| ^VERIFICATION SUCCESSFUL$ |
There was a problem hiding this comment.
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.
There was a problem hiding this comment.
I have added patterns that must not be found in test.desc, so I think this is addressed.
| Author: Michael Tautschnig | ||
| Date: April 2017 |
There was a problem hiding this comment.
This comment block doesn't normally have the date, how come we've added it here?
There was a problem hiding this comment.
$ git grep ^Date: | wc -l
152
Seems it's all very much inconsistent.
|
|
||
| #include <goto-programs/goto_functions.h> | ||
|
|
||
| #include "remove_function.h" |
tautschnig
force-pushed
the
inspect-functions
branch
from
14875e9 to
50d3563
Compare
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
force-pushed
the
inspect-functions
branch
from
50d3563 to
accc412
Compare
3 participants
No description provided.