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

#include <local_bitvector_analysis.h>

+ Collaboration diagram for local_bitvector_analysist:

Classes

struct  flagst
 

Public Types

typedef goto_functionst::goto_functiont goto_functiont
 

Public Member Functions

 local_bitvector_analysist (const goto_functiont &_goto_function, const namespacet &ns)
 
void output (std::ostream &out, const goto_functiont &goto_function, const namespacet &ns) const
 
flagst get (const goto_programt::const_targett t, const exprt &src)
 

Public Attributes

dirtyt dirty
 
localst locals
 
local_cfgt cfg
 

Protected Types

typedef expanding_vectort< flagst > points_tot
 
typedef std::vector< points_tot > loc_infost
 

Protected Member Functions

void build ()
 
void assign_lhs (const exprt &lhs, const exprt &rhs, points_tot &loc_info_src, points_tot &loc_info_dest)
 
flagst get_rec (const exprt &rhs, points_tot &loc_info_src)
 
bool is_tracked (const irep_idt &identifier)
 

Static Protected Member Functions

static bool merge (points_tot &a, points_tot &b)
 

Protected Attributes

const namespacet & ns
 
numberingt< irep_idt > pointers
 
loc_infost loc_infos
 

Detailed Description

Definition at line 22 of file local_bitvector_analysis.h.

Member Typedef Documentation

◆ goto_functiont

typedef goto_functionst::goto_functiont local_bitvector_analysist::goto_functiont

Definition at line 25 of file local_bitvector_analysis.h.

◆ loc_infost

typedef std::vector<points_tot> local_bitvector_analysist::loc_infost
protected

Definition at line 191 of file local_bitvector_analysis.h.

◆ points_tot

typedef expanding_vectort<flagst> local_bitvector_analysist::points_tot
protected

Definition at line 187 of file local_bitvector_analysis.h.

Constructor & Destructor Documentation

◆ local_bitvector_analysist()

local_bitvector_analysist::local_bitvector_analysist ( const goto_functiont &  _goto_function,
const namespacet &  ns 
)
inline

Definition at line 27 of file local_bitvector_analysis.h.

Member Function Documentation

◆ assign_lhs()

void local_bitvector_analysist::assign_lhs ( const exprt &  lhs,
const exprt &  rhs,
points_tot &  loc_info_src,
points_tot &  loc_info_dest 
)
protected

Definition at line 62 of file local_bitvector_analysis.cpp.

◆ build()

void local_bitvector_analysist::build ( )
protected

Definition at line 237 of file local_bitvector_analysis.cpp.

◆ get()

local_bitvector_analysist::flagst local_bitvector_analysist::get ( const goto_programt::const_targett  t,
const exprt &  src 
)

Definition at line 102 of file local_bitvector_analysis.cpp.

◆ get_rec()

local_bitvector_analysist::flagst local_bitvector_analysist::get_rec ( const exprt &  rhs,
points_tot &  loc_info_src 
)
protected

Definition at line 112 of file local_bitvector_analysis.cpp.

◆ is_tracked()

bool local_bitvector_analysist::is_tracked ( const irep_idt &  identifier)
protected
Returns
return 'true' iff we track the object with given identifier

Definition at line 55 of file local_bitvector_analysis.cpp.

◆ merge()

bool local_bitvector_analysist::merge ( points_tot &  a,
points_tot &  b 
)
staticprotected

Definition at line 41 of file local_bitvector_analysis.cpp.

◆ output()

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

Definition at line 343 of file local_bitvector_analysis.cpp.

Member Data Documentation

◆ cfg

local_cfgt local_bitvector_analysist::cfg

Definition at line 45 of file local_bitvector_analysis.h.

◆ dirty

dirtyt local_bitvector_analysist::dirty

Definition at line 43 of file local_bitvector_analysis.h.

◆ loc_infos

loc_infost local_bitvector_analysist::loc_infos
protected

Definition at line 192 of file local_bitvector_analysis.h.

◆ locals

localst local_bitvector_analysist::locals

Definition at line 44 of file local_bitvector_analysis.h.

◆ ns

const namespacet& local_bitvector_analysist::ns
protected

Definition at line 180 of file local_bitvector_analysis.h.

◆ pointers

numberingt<irep_idt> local_bitvector_analysist::pointers
protected

Definition at line 183 of file local_bitvector_analysis.h.

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