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

numberingt< exprt, irep_hashobjects
 
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

◆ 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

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

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.

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 140 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 320 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 167 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 463 of file local_may_alias.cpp.

Member Data Documentation

◆ cfg

local_cfgt local_may_aliast::cfg

Definition at line 45 of file local_may_alias.h.

◆ dirty

dirtyt local_may_aliast::dirty

Definition at line 43 of file local_may_alias.h.

◆ loc_infos

loc_infost local_may_aliast::loc_infos
protected

Definition at line 76 of file local_may_alias.h.

◆ locals

localst local_may_aliast::locals

Definition at line 44 of file local_may_alias.h.

◆ objects

numberingt<exprt, irep_hash> local_may_aliast::objects
mutableprotected

Definition at line 62 of file local_may_alias.h.

◆ unknown_object

unsigned local_may_aliast::unknown_object
protected

Definition at line 91 of file local_may_alias.h.


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