Constant propagator: add callback to filter tracked values #2520
Conversation
smowton
requested review from
chrisr-diffblue,
martin-cs,
peterschrammel and
thk123
as code owners
There was a problem hiding this comment.
Passed Diffblue compatibility checks (cbmc commit: b96dd06).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/78102658
smowton
force-pushed
the
smowton/feature/constant-propagator-selectivity
branch
from
b96dd06 to
0930b0d
Compare
|
|
||
| #include <util/message.h> | ||
|
|
||
| #include <iostream> |
There was a problem hiding this comment.
Why is iostream imported here?
There was a problem hiding this comment.
Because I'm silly, is why
There was a problem hiding this comment.
Wait no I'm not, this is used as the output for goto_convert
There was a problem hiding this comment.
Please don't. Unit tests have become very hard see failures in as they generate a ton of noise. Tests must be completely silent by default. If there is an error, then it should be reported, but not in any other case. As such: please report to a std::ostringstream and check that that output is empty.
A user may supply a predicate, in which case the constant propagator will only track symbols that pass the predicate. For example, one out-of-tree user uses this to restrict propagation to globals.
smowton
force-pushed
the
smowton/feature/constant-propagator-selectivity
branch
from
0930b0d to
56a487e
Compare
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: 0930b0d).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/78210227
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.
Common spurious failures:
- the cbmc commit has disappeared in the mean time (e.g. in a force-push)
- the author is not in the list of contributors (e.g. first-time contributors).
There was a problem hiding this comment.
Passed Diffblue compatibility checks (cbmc commit: 56a487e).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/78212385
6409eae Merge pull request diffblue#2449 from tautschnig/c++-template-cleanup 1134455 Merge pull request diffblue#2443 from tautschnig/vs-rdecl 6e9e655 Merge pull request diffblue#2520 from smowton/smowton/feature/constant-propagator-selectivity 9013779 Merge pull request diffblue#2383 from tautschnig/no-sed 56a487e Constant propagator: add callback to filter tracked values a354513 Merge pull request diffblue#2510 from polgreen/hex_trace 3545be4 Merge pull request diffblue#2523 from peterschrammel/do-not-ignore-full-slice 819c683 Merge pull request diffblue#2493 from jeannielynnmoulton/jeannie/InnerClasses a018652 allow unsigned long instead of unsigned in regression test for hex_trace d5bbdd8 represent numerical values in CBMC trace in hex 19bddce Do not ignore --full-slice 5350133 Refactor inner class parsing. 6e554d9 Merge pull request diffblue#2500 from diffblue/git-version-speedup 9ba55e2 Marks anonymous classes as inner classes b96c7ba move build commands for version.h from common to util/ 6ce7b13 Clarifies language in documentation. c0c1029 Fixes parsing for anonymous classes 1930aef Refactors parsing of inner classes attribute. b28562b Adds unit test for parsing inner classes. c336455 Stores inner class data in java class types. 457bac9 Parses InnerClasses attribute of java bytecode. 34bd58f Clean up unused template instantiation symbols fea1f47 Remove unused parameter from rDeclarator e00c6ee Set BUILD_ENV via make variable instead of patching via sed git-subtree-dir: cbmc git-subtree-split: 6409eae
A user may supply a predicate, in which case the constant propagator will only track symbols that pass the predicate. The security product currently uses this to do const prop only over global variables.
This incidentally also regularises the constructors for
constant_propagator_ait, so there is a side-effecting and a non-side-effecting version for both whole-model and single-function cases.