Do not instrument built-ins #292
Conversation
peterschrammel
assigned kroening and peterschrammel and unassigned kroening and peterschrammel
src/goto-instrument/cover.cpp
Outdated
| @@ -1375,9 +1390,10 @@ void instrument_cover_goals( | |||
| Forall_goto_functions(f_it, goto_functions) | |||
| { | |||
| if(f_it->first==ID__start || | |||
| f_it->first=="__CPROVER_initialize") | |||
| f_it->first=="__CPROVER_initialize" || | |||
There was a problem hiding this comment.
Use CPROVER_PREFIX "initialize" (and #include <util/cprover_prefix.h>) [yes, there are ~2000 other locations where that should get fixed]
src/goto-programs/remove_returns.cpp
Outdated
| @@ -185,7 +185,7 @@ void remove_returnst::do_function_calls( | |||
| t_a->code=code_assignt(function_call.lhs(), rhs); | |||
| t_a->function=i_it->function; | |||
|
|
|||
| // fry the previous assignment | |||
| // try the previous assignment | |||
There was a problem hiding this comment.
I do not think that was a typo!?
|
I think this PR might need some rework as we've now got a different way of determining built-ins. |
peterschrammel
force-pushed
the
do-not-instrument-built-ins
branch
7 times, most recently
from
815ec19 to
4e43a15
Compare
|
@tautschnig, fixed. |
peterschrammel
force-pushed
the
do-not-instrument-built-ins
branch
from
4e43a15 to
a1ac2ec
Compare
|
@peterschrammel Would you mind rebasing to get all fixes from master such as to repair the AppVeyor failure? The irep_ids merge teaches me that we should have all tests succeed before accepting. Thanks! |
peterschrammel
force-pushed
the
do-not-instrument-built-ins
branch
from
a1ac2ec to
0c5b645
Compare
|
It seems a large number of tests have blank lines. I'm working on a PR to remedy this. |
|
How are tests with blank lines related to this PR? |
|
Rebasing... |
peterschrammel
force-pushed
the
do-not-instrument-built-ins
branch
from
0c5b645 to
9dacdb1
Compare
|
The blank lines weren't related - current master is/was still broken... |
…ing cover instrumentation fixes diffblue#259
peterschrammel
force-pushed
the
do-not-instrument-built-ins
branch
from
9dacdb1 to
12d6582
Compare
|
@tautschnig, all green now. |
Merge latest cbmc/develop into cbmc subtree
fixes #259