cprover
|
#include <local_bitvector_analysis.h>
Classes | |
struct | flagst |
class | loc_infot |
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< loc_infot > | loc_infost |
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) |
flagst | get_rec (const exprt &rhs, const loc_infot &loc_info_src) |
bool | is_tracked (const irep_idt &identifier) |
Protected Attributes | |
numbering< irep_idt > | pointers |
loc_infost | loc_infos |
Definition at line 23 of file local_bitvector_analysis.h.
typedef goto_functionst::goto_functiont local_bitvector_analysist::goto_functiont |
Definition at line 26 of file local_bitvector_analysis.h.
|
protected |
Definition at line 198 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(), numbering< T >::number(), pointers, local_bitvector_analysist::loc_infot::points_to, to_if_expr(), to_index_expr(), to_member_expr(), to_symbol_expr(), and to_typecast_expr().
Referenced by build().
|
protected |
Definition at line 246 of file local_bitvector_analysis.cpp.
References ASSIGN, assign_lhs(), cfg, DEAD, DECL, FUNCTION_CALL, irept::is_not_nil(), is_tracked(), code_assignt::lhs(), code_function_callt::lhs(), loc_infos, locals, localst::locals_map, local_bitvector_analysist::flagst::mk_unknown(), local_cfgt::nodes, numbering< T >::number(), 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(), and to_code_function_call().
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 125 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(), numbering< T >::number(), address_of_exprt::object(), exprt::op0(), exprt::op1(), exprt::operands(), pointers, local_bitvector_analysist::loc_infot::points_to, 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().
void local_bitvector_analysist::output | ( | std::ostream & | out, |
const goto_functiont & | goto_function, | ||
const namespacet & | ns | ||
) | const |
Definition at line 329 of file local_bitvector_analysis.cpp.
References forall_goto_program_instructions, loc_infos, pointers, and local_bitvector_analysist::loc_infot::points_to.
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 199 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().