cprover
|
#include <local_bitvector_analysis.h>
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 std::stack< unsigned > | work_queuet |
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 |
numbering< irep_idt > | pointers |
loc_infost | loc_infos |
Definition at line 23 of file local_bitvector_analysis.h.
Definition at line 26 of file local_bitvector_analysis.h.
|
protected |
Definition at line 194 of file local_bitvector_analysis.h.
|
protected |
Definition at line 190 of file local_bitvector_analysis.h.
|
protected |
Definition at line 184 of file local_bitvector_analysis.h.
|
inline |
Definition at line 28 of file local_bitvector_analysis.h.
|
protected |
Definition at line 68 of file local_bitvector_analysis.cpp.
|
protected |
Definition at line 244 of file local_bitvector_analysis.cpp.
local_bitvector_analysist::flagst local_bitvector_analysist::get | ( | const goto_programt::const_targett | t, |
const exprt & | src | ||
) |
Definition at line 108 of file local_bitvector_analysis.cpp.
|
protected |
Definition at line 119 of file local_bitvector_analysis.cpp.
|
protected |
Definition at line 61 of file local_bitvector_analysis.cpp.
|
staticprotected |
Definition at line 44 of file local_bitvector_analysis.cpp.
void local_bitvector_analysist::output | ( | std::ostream & | out, |
const goto_functiont & | goto_function, | ||
const namespacet & | ns | ||
) | const |
Definition at line 358 of file local_bitvector_analysis.cpp.
local_cfgt local_bitvector_analysist::cfg |
Definition at line 46 of file local_bitvector_analysis.h.
dirtyt local_bitvector_analysist::dirty |
Definition at line 44 of file local_bitvector_analysis.h.
|
protected |
Definition at line 195 of file local_bitvector_analysis.h.
localst local_bitvector_analysist::locals |
Definition at line 45 of file local_bitvector_analysis.h.
|
protected |
Definition at line 181 of file local_bitvector_analysis.h.
Definition at line 186 of file local_bitvector_analysis.h.