CBMC
|
Public Member Functions | |
uninitializedt (symbol_table_baset &_symbol_table) | |
void | add_assertions (const irep_idt &function_identifer, 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_table_baset & | symbol_table |
namespacet | ns |
uninitialized_analysist | uninitialized_analysis |
std::set< irep_idt > | tracking |
Definition at line 18 of file uninitialized.cpp.
|
inlineexplicit |
Definition at line 21 of file uninitialized.cpp.
void uninitializedt::add_assertions | ( | const irep_idt & | function_identifer, |
goto_programt & | goto_program | ||
) |
Definition at line 63 of file uninitialized.cpp.
|
protected |
which variables need tracking, i.e., are uninitialized and may be read?
Definition at line 43 of file uninitialized.cpp.
|
protected |
Definition at line 32 of file uninitialized.cpp.
|
protected |
Definition at line 31 of file uninitialized.cpp.
|
protected |
Definition at line 37 of file uninitialized.cpp.
|
protected |
Definition at line 33 of file uninitialized.cpp.