CBMC
Classes | Public Types | Public Member Functions | Public Attributes | Protected Types | Protected Member Functions | Protected Attributes | List of all members
local_may_aliast Class Reference

#include <local_may_alias.h>

+ Collaboration diagram for local_may_aliast:

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< exprt > get (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_nrt > work_queuet
 
typedef unsigned_union_find alias_sett
 
typedef std::vector< loc_infot > loc_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

numberingt< exprt, irep_hash > objects
 
loc_infost loc_infos
 
unsigned unknown_object
 

Detailed Description

Definition at line 25 of file local_may_alias.h.

Member Typedef Documentation

◆ alias_sett

typedef unsigned_union_find local_may_aliast::alias_sett
protected

Definition at line 65 of file local_may_alias.h.

◆ goto_functiont

typedef goto_functionst::goto_functiont local_may_aliast::goto_functiont

Definition at line 28 of file local_may_alias.h.

◆ loc_infost

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

Definition at line 76 of file local_may_alias.h.

◆ object_sett

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

Definition at line 85 of file local_may_alias.h.

◆ work_queuet

typedef std::stack<local_cfgt::node_nrt> local_may_aliast::work_queuet
protected

Definition at line 61 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 30 of file local_may_alias.h.

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.

◆ assign_lhs()

void local_may_aliast::assign_lhs ( const exprt &  lhs,
const exprt &  rhs,
const loc_infot &  loc_info_src,
loc_infot &  loc_info_dest 
)
protected

Definition at line 44 of file local_may_alias.cpp.

◆ build()

void local_may_aliast::build ( const goto_functiont &  goto_function)
protected

Definition at line 322 of file local_may_alias.cpp.

◆ get()

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

Definition at line 115 of file local_may_alias.cpp.

◆ get_rec()

void local_may_aliast::get_rec ( object_sett &  dest,
const exprt &  rhs,
const loc_infot &  loc_info_src 
) const
protected

Definition at line 169 of file local_may_alias.cpp.

◆ output()

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

Definition at line 465 of file local_may_alias.cpp.

Member Data Documentation

◆ cfg

local_cfgt local_may_aliast::cfg

Definition at line 46 of file local_may_alias.h.

◆ dirty

dirtyt local_may_aliast::dirty

Definition at line 44 of file local_may_alias.h.

◆ loc_infos

loc_infost local_may_aliast::loc_infos
protected

Definition at line 77 of file local_may_alias.h.

◆ locals

localst local_may_aliast::locals

Definition at line 45 of file local_may_alias.h.

◆ objects

numberingt<exprt, irep_hash> local_may_aliast::objects
mutableprotected

Definition at line 63 of file local_may_alias.h.

◆ unknown_object

unsigned local_may_aliast::unknown_object
protected

Definition at line 92 of file local_may_alias.h.

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