|
CBMC
|
Include dependency graph for constant_propagator.h:
This graph shows which files directly or indirectly include this file:Go to the source code of this file.
Classes | |
| class | constant_propagator_domaint |
| struct | constant_propagator_domaint::valuest |
| class | constant_propagator_ait |
Constant propagation
A simple, unsound constant propagator. Assignments to symbols (local and global variables) are tracked, and propagated if a unique value is found at a given use site. Function calls are accounted for (they are assumed to overwrite all address-taken variables; see dirtyt), but assignments through pointers are not (they are assumed to have no effect).
Can be restricted to operate over only particular symbols by passing a predicate to a constant_propagator_ait constructor, in which case this can be rendered sound by restricting it to non-address-taken variables.
Definition in file constant_propagator.h.