cprover
|
Public Member Functions | |
uninitializedt (symbol_tablet &_symbol_table) | |
void | add_assertions (goto_programt &goto_program) |
Protected Member Functions | |
void | get_tracking (goto_programt::const_targett i_it) |
which variables need tracking, i.e., are uninitialized and may be read? More... | |
Protected Attributes | |
symbol_tablet & | symbol_table |
namespacet | ns |
uninitialized_analysist | uninitialized_analysis |
std::set< irep_idt > | tracking |
Definition at line 22 of file uninitialized.cpp.
|
inlineexplicit |
Definition at line 25 of file uninitialized.cpp.
void uninitializedt::add_assertions | ( | goto_programt & | goto_program | ) |
Definition at line 66 of file uninitialized.cpp.
References ASSERT, ASSIGN, symbolt::base_name, goto_programt::instructiont::code, DECL, forall_goto_program_instructions, Forall_goto_program_instructions, symbol_exprt::get_identifier(), code_declt::get_identifier(), get_tracking(), goto_program, goto_programt::instructiont::guard, id2string(), symbol_tablet::insert(), goto_programt::insert_after(), goto_programt::insert_before_swap(), goto_programt::instructiont::is_decl(), symbolt::is_file_local, symbolt::is_lvalue, symbolt::is_static_lifetime, symbolt::is_thread_local, symbolt::location, namespacet::lookup(), symbolt::mode, symbolt::module, symbolt::name, ns, objects_read(), objects_written(), source_locationt::set_comment(), symbol_exprt::set_identifier(), source_locationt::set_property_class(), goto_programt::instructiont::source_location, symbol_table, to_code_decl(), to_symbol_expr(), tracking, symbolt::type, exprt::type(), goto_programt::instructiont::type, and uninitialized_analysis.
Referenced by add_uninitialized_locals_assertions().
|
protected |
which variables need tracking, i.e., are uninitialized and may be read?
Definition at line 46 of file uninitialized.cpp.
References symbol_exprt::get_identifier(), objects_read(), to_symbol_expr(), tracking, and uninitialized_analysis.
Referenced by add_assertions().
|
protected |
Definition at line 35 of file uninitialized.cpp.
Referenced by add_assertions().
|
protected |
Definition at line 34 of file uninitialized.cpp.
Referenced by add_assertions().
|
protected |
Definition at line 40 of file uninitialized.cpp.
Referenced by add_assertions(), and get_tracking().
|
protected |
Definition at line 36 of file uninitialized.cpp.
Referenced by add_assertions(), and get_tracking().