Do not instrument built-ins #292
Conversation
peterschrammel
assigned
kroening and
peterschrammel and unassigned
kroening and
peterschrammel
tautschnig
left a comment
tautschnig
left a comment
There was a problem hiding this comment.
The "typo" commit may not be appropriate; other comments are minor, and a rebase is necessary.
src/goto-instrument/cover.cpp
Outdated
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
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
3 participants
fixes #259