Range-based reaching definitions analysis (following Field- Sensitive Program Dependence Analysis, Litvak et al., FSE 2010) More...
Include dependency graph for reaching_definitions.h: This graph shows which files directly or indirectly include this file:Go to the source code of this file.
Classes | |
| class | sparse_bitvector_analysist< V > |
An instance of this class provides an assignment of unique numeric ID to each inserted reaching_definitiont instance. More... | |
| struct | reaching_definitiont |
| Identifies a GOTO instruction where a given variable is defined (i.e. More... | |
| class | rd_range_domaint |
Because the class is inherited from ai_domain_baset, its instance represents an element of a domain of the reaching definitions abstract interpretation analysis. More... | |
| class | reaching_definitions_analysist |
Functions | |
| bool | operator< (const reaching_definitiont &a, const reaching_definitiont &b) |
| In order to use instances of this structure as keys in ordered containers, such as std::map, an ordering is defined. More... | |
Detailed Description
Range-based reaching definitions analysis (following Field- Sensitive Program Dependence Analysis, Litvak et al., FSE 2010)
This module implements the reaching definitions data-flow analysis (see https://en.wikipedia.org/wiki/Reaching_definition for basic introduction) on multi-threaded GOTO programs.
The domain element is defined in a class rd_range_domaint and the actual analysis is implemented in a class reaching_definitions_analysist. Beside these classes there are more data structures necessary in the computation. We discuss all of them in the following sub-sections.
Definition in file reaching_definitions.h.
Function Documentation
◆ operator<()
|
inline |
In order to use instances of this structure as keys in ordered containers, such as std::map, an ordering is defined.
Definition at line 113 of file reaching_definitions.h.
