CBMC
reaching_definitions.cpp File Reference

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

Detailed Description

Range-based reaching definitions analysis (following Field- Sensitive Program Dependence Analysis, Litvak et al., FSE 2010)

Definition in file reaching_definitions.cpp.