cprover
local_may_aliast Class Reference

#include <local_may_alias.h>

Collaboration diagram for local_may_aliast:
[legend]

Classes

class  loc_infot
 

Public Types

typedef goto_functionst::goto_functiont goto_functiont
 

Public Member Functions

 local_may_aliast (const goto_functiont &_goto_function)
 
void output (std::ostream &out, const goto_functiont &goto_function, const namespacet &ns) const
 
std::set< exprtget (const goto_programt::const_targett t, const exprt &src) const
 
bool aliases (const goto_programt::const_targett t, const exprt &src1, const exprt &src2) const
 

Public Attributes

dirtyt dirty
 
localst locals
 
local_cfgt cfg
 

Protected Types

typedef std::stack< local_cfgt::node_nrtwork_queuet
 
typedef unsigned_union_find alias_sett
 
typedef std::vector< loc_infotloc_infost
 
typedef std::set< unsigned > object_sett
 

Protected Member Functions

void build (const goto_functiont &goto_function)
 
void assign_lhs (const exprt &lhs, const exprt &rhs, const loc_infot &loc_info_src, loc_infot &loc_info_dest)
 
void get_rec (object_sett &dest, const exprt &rhs, const loc_infot &loc_info_src) const
 

Protected Attributes

numbering< exprtobjects
 
loc_infost loc_infos
 
unsigned unknown_object
 

Detailed Description

Definition at line 24 of file local_may_alias.h.

Member Typedef Documentation

§ alias_sett

Definition at line 64 of file local_may_alias.h.

§ goto_functiont

typedef goto_functionst::goto_functiont local_may_aliast::goto_functiont

Definition at line 27 of file local_may_alias.h.

§ loc_infost

typedef std::vector<loc_infot> local_may_aliast::loc_infost
protected

Definition at line 75 of file local_may_alias.h.

§ object_sett

typedef std::set<unsigned> local_may_aliast::object_sett
protected

Definition at line 84 of file local_may_alias.h.

§ work_queuet

Definition at line 60 of file local_may_alias.h.

Constructor & Destructor Documentation

§ local_may_aliast()

local_may_aliast::local_may_aliast ( const goto_functiont _goto_function)
inlineexplicit

Definition at line 29 of file local_may_alias.h.

References build(), and output().

Referenced by local_may_alias_factoryt::operator()().

Member Function Documentation

§ aliases()

bool local_may_aliast::aliases ( const goto_programt::const_targett  t,
const exprt src1,
const exprt src2 
) const

Definition at line 141 of file local_may_alias.cpp.

References cfg, get_rec(), loc_infos, local_cfgt::loc_map, and unknown_object.

§ assign_lhs()

§ build()

§ get()

std::set< exprt > local_may_aliast::get ( const goto_programt::const_targett  t,
const exprt src 
) const

§ get_rec()

§ output()

void local_may_aliast::output ( std::ostream &  out,
const goto_functiont goto_function,
const namespacet ns 
) const

Member Data Documentation

§ cfg

local_cfgt local_may_aliast::cfg

Definition at line 45 of file local_may_alias.h.

Referenced by aliases(), build(), and get().

§ dirty

dirtyt local_may_aliast::dirty

Definition at line 43 of file local_may_alias.h.

Referenced by assign_lhs(), and build().

§ loc_infos

loc_infost local_may_aliast::loc_infos
protected

Definition at line 76 of file local_may_alias.h.

Referenced by aliases(), build(), get(), and output().

§ locals

localst local_may_aliast::locals

Definition at line 44 of file local_may_alias.h.

Referenced by assign_lhs(), and build().

§ objects

numbering<exprt> local_may_aliast::objects
mutableprotected

Definition at line 62 of file local_may_alias.h.

Referenced by assign_lhs(), build(), get(), get_rec(), and output().

§ unknown_object

unsigned local_may_aliast::unknown_object
protected

Definition at line 91 of file local_may_alias.h.

Referenced by aliases(), assign_lhs(), build(), and get_rec().


The documentation for this class was generated from the following files: