|
CBMC
|
Range-based reaching definitions analysis (following Field- Sensitive Program Dependence Analysis, Litvak et al., FSE 2010) More...
#include "reaching_definitions.h"#include <util/base_exceptions.h>#include <util/pointer_offset_size.h>#include <pointer-analysis/value_set_analysis_fi.h>#include "dirty.h"#include "is_threaded.h"#include <memory>
Include dependency graph for reaching_definitions.cpp:Go to the source code of this file.
Classes | |
| class | rd_range_domain_factoryt |
| This ensures that all domains are constructed with the appropriate pointer back to the analysis engine itself. More... | |
Range-based reaching definitions analysis (following Field- Sensitive Program Dependence Analysis, Litvak et al., FSE 2010)
Definition in file reaching_definitions.cpp.