52 if(o_it->id()==ID_symbol)
55 const std::set<irep_idt> &uninitialized=
57 if(uninitialized.find(identifier)!=uninitialized.end())
60 else if(o_it->id()==ID_dereference)
77 for(std::set<irep_idt>::const_iterator
101 goto_programt::instructiont &instruction=*i_it;
103 if(instruction.is_decl())
124 i1->source_location=instruction.source_location;
128 i2->source_location=instruction.source_location;
141 const std::set<irep_idt> &uninitialized=
147 if(it->id()==ID_symbol)
151 if(uninitialized.find(identifier)!=uninitialized.end())
157 goto_programt::instructiont assertion;
160 assertion.source_location=instruction.source_location;
161 assertion.source_location.set_comment(
162 "use of uninitialized local variable");
163 assertion.source_location.set_property_class(
"uninitialized local");
174 if(it->id()==ID_symbol)
182 goto_programt::instructiont assignment;
186 assignment.source_location=instruction.source_location;
218 if(f_it->second.body_available())
221 out <<
"//// Function: " << f_it->first <<
'\n';
224 uninitialized_analysis(f_it->second.body, ns);
225 uninitialized_analysis.
output(ns, f_it->second.body, out);
irep_idt name
The unique identifier.
Detection for Uninitialized Local Variables.
const code_declt & to_code_decl(const codet &code)
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
const std::string & id2string(const irep_idt &d)
void show_uninitialized(const class symbol_tablet &symbol_table, const goto_functionst &goto_functions, std::ostream &out)
uninitializedt(symbol_tablet &_symbol_table)
irep_idt mode
Language mode.
void get_tracking(goto_programt::const_targett i_it)
which variables need tracking, i.e., are uninitialized and may be read?
symbol_tablet & symbol_table
const irep_idt & get_identifier() const
irep_idt module
Name of module the symbol belongs to.
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
void add_uninitialized_locals_assertions(symbol_tablet &symbol_table, goto_functionst &goto_functions)
virtual void output(const namespacet &ns, const goto_functionst &goto_functions, std::ostream &out) const
instructionst::const_iterator const_targett
The boolean constant true.
A declaration of a local variable.
API to expression classes.
std::set< irep_idt > tracking
const irep_idt & get_identifier() const
void objects_read(const exprt &src, std::list< exprt > &dest)
targett insert_after(const_targett target)
Insertion after the given target.
#define forall_expr_list(it, expr)
bool move(symbolt &symbol, symbolt *&new_symbol)
Move a symbol into the symbol table.
Detection for Uninitialized Local Variables.
The boolean constant false.
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
typet type
Type of symbol.
source_locationt location
Source code location of definition of symbol.
irep_idt base_name
Base (non-scoped) name.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
#define Forall_goto_functions(it, functions)
void objects_written(const exprt &src, std::list< exprt > &dest)
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
void set_identifier(const irep_idt &identifier)
#define Forall_goto_program_instructions(it, program)
Expression to hold a symbol (variable)
void add_assertions(goto_programt &goto_program)
uninitialized_analysist uninitialized_analysis
#define forall_goto_functions(it, functions)
#define forall_goto_program_instructions(it, program)
instructionst::iterator targett