cprover
|
Detection for Uninitialized Local Variables. More...
#include "uninitialized.h"
#include <util/std_code.h>
#include <util/std_expr.h>
#include <util/symbol_table.h>
#include <analyses/uninitialized_domain.h>
Go to the source code of this file.
Classes | |
class | uninitializedt |
Functions | |
void | add_uninitialized_locals_assertions (goto_modelt &goto_model) |
void | show_uninitialized (const goto_modelt &goto_model, std::ostream &out) |
Detection for Uninitialized Local Variables.
Definition in file uninitialized.cpp.
void add_uninitialized_locals_assertions | ( | goto_modelt & | goto_model | ) |
Definition at line 197 of file uninitialized.cpp.
References uninitializedt::add_assertions(), Forall_goto_functions, goto_modelt::goto_functions, and goto_modelt::symbol_table.
Referenced by goto_instrument_parse_optionst::instrument_goto_program().
void show_uninitialized | ( | const goto_modelt & | goto_model, |
std::ostream & | out | ||
) |
Definition at line 207 of file uninitialized.cpp.
References forall_goto_functions, goto_modelt::goto_functions, ai_baset::output(), and goto_modelt::symbol_table.
Referenced by goto_instrument_parse_optionst::doit().