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, DECL, forall_expr_list, forall_goto_program_instructions, Forall_goto_program_instructions, symbol_exprt::get_identifier(), code_declt::get_identifier(), get_tracking(), id2string(), goto_program_templatet< codeT, guardT >::insert_after(), goto_program_templatet< codeT, guardT >::insert_before_swap(), symbolt::is_file_local, symbolt::is_lvalue, symbolt::is_static_lifetime, symbolt::is_thread_local, symbolt::location, namespacet::lookup(), symbolt::mode, symbolt::module, symbol_tablet::move(), symbolt::name, ns, objects_read(), objects_written(), symbol_exprt::set_identifier(), symbol_table, to_code_decl(), to_symbol_expr(), tracking, symbolt::type, exprt::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 forall_expr_list, 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().