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) | |
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 (const goto_functiont &goto_function) |
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 | |
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 191 of file local_bitvector_analysis.h.
|
protected |
Definition at line 187 of file local_bitvector_analysis.h.
|
protected |
Definition at line 181 of file local_bitvector_analysis.h.
|
inlineexplicit |
Definition at line 28 of file local_bitvector_analysis.h.
References build().
|
protected |
Definition at line 72 of file local_bitvector_analysis.cpp.
References symbol_exprt::get_identifier(), get_rec(), irept::id(), is_tracked(), pointers, to_if_expr(), to_index_expr(), to_member_expr(), to_symbol_expr(), and to_typecast_expr().
Referenced by build().
|
protected |
Definition at line 244 of file local_bitvector_analysis.cpp.
References ASSIGN, assign_lhs(), cfg, goto_programt::instructiont::code, DEAD, DECL, FUNCTION_CALL, irept::is_not_nil(), is_tracked(), code_assignt::lhs(), code_function_callt::lhs(), loc_infos, locals, localst::locals_map, merge(), local_bitvector_analysist::flagst::mk_unknown(), local_cfgt::nodes, pointers, code_assignt::rhs(), local_cfgt::nodet::successors, code_declt::symbol(), code_deadt::symbol(), local_cfgt::nodet::t, to_code_assign(), to_code_dead(), to_code_decl(), to_code_function_call(), and goto_programt::instructiont::type.
Referenced by local_bitvector_analysist().
local_bitvector_analysist::flagst local_bitvector_analysist::get | ( | const goto_programt::const_targett | t, |
const exprt & | src | ||
) |
Definition at line 112 of file local_bitvector_analysis.cpp.
References cfg, get_rec(), loc_infos, and local_cfgt::loc_map.
Referenced by goto_checkt::goto_check(), and goto_checkt::pointer_validity_check().
|
protected |
Definition at line 123 of file local_bitvector_analysis.cpp.
References index_exprt::array(), symbol_exprt::get_identifier(), side_effect_exprt::get_statement(), irept::id(), localst::is_local(), is_tracked(), exprt::is_zero(), locals, local_bitvector_analysist::flagst::mk_dynamic_heap(), local_bitvector_analysist::flagst::mk_dynamic_local(), local_bitvector_analysist::flagst::mk_integer_address(), local_bitvector_analysist::flagst::mk_null(), local_bitvector_analysist::flagst::mk_static_lifetime(), local_bitvector_analysist::flagst::mk_uninitialized(), local_bitvector_analysist::flagst::mk_unknown(), local_bitvector_analysist::flagst::mk_uses_offset(), address_of_exprt::object(), exprt::op0(), exprt::op1(), exprt::operands(), pointers, to_address_of_expr(), to_index_expr(), to_side_effect_expr(), to_symbol_expr(), to_typecast_expr(), and exprt::type().
Referenced by assign_lhs(), and get().
|
protected |
Definition at line 61 of file local_bitvector_analysis.cpp.
References dirty, locals, and localst::locals_map.
Referenced by assign_lhs(), build(), and get_rec().
|
staticprotected |
Definition at line 44 of file local_bitvector_analysis.cpp.
References expanding_vectort< T >::size().
Referenced by build().
void local_bitvector_analysist::output | ( | std::ostream & | out, |
const goto_functiont & | goto_function, | ||
const namespacet & | ns | ||
) | const |
Definition at line 327 of file local_bitvector_analysis.cpp.
References goto_functiont::body, forall_goto_program_instructions, loc_infos, goto_programt::output_instruction(), and pointers.
Referenced by goto_instrument_parse_optionst::doit().
local_cfgt local_bitvector_analysist::cfg |
Definition at line 44 of file local_bitvector_analysis.h.
dirtyt local_bitvector_analysist::dirty |
Definition at line 42 of file local_bitvector_analysis.h.
Referenced by goto_checkt::goto_check(), and is_tracked().
|
protected |
Definition at line 192 of file local_bitvector_analysis.h.
localst local_bitvector_analysist::locals |
Definition at line 43 of file local_bitvector_analysis.h.
Referenced by build(), get_rec(), and is_tracked().
Definition at line 183 of file local_bitvector_analysis.h.
Referenced by assign_lhs(), build(), get_rec(), and output().