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>
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.