CBMC
dependence_graph.cpp File Reference

Field-Sensitive Program Dependence Analysis, Litvak et al., FSE 2010. More...

#include "dependence_graph.h"
#include <util/container_utils.h>
#include <util/json_irep.h>
#include "goto_rw.h"
+ Include dependency graph for dependence_graph.cpp:

Go to the source code of this file.

Classes

class  dep_graph_domain_factoryt
 This ensures that all domains are constructed with the node ID that links them to the graph part of the dependency graph. More...
 

Functions

static bool may_be_def_use_pair (const range_spect &w_start, const range_spect &w_end, const range_spect &r_start, const range_spect &r_end)
 

Detailed Description

Field-Sensitive Program Dependence Analysis, Litvak et al., FSE 2010.

Definition in file dependence_graph.cpp.

Function Documentation

◆ may_be_def_use_pair()

static bool may_be_def_use_pair ( const range_spect w_start,
const range_spect w_end,
const range_spect r_start,
const range_spect r_end 
)
static

Definition at line 127 of file dependence_graph.cpp.