52 for(
const auto &
object : objects)
54 if(
object.
id() == ID_symbol)
57 const std::set<irep_idt> &uninitialized=
59 if(uninitialized.find(identifier)!=uninitialized.end())
62 else if(
object.
id() == ID_dereference)
81 for(std::set<irep_idt>::const_iterator
145 const std::set<irep_idt> &uninitialized=
149 for(
const auto &
object : read)
151 if(
object.
id() == ID_symbol)
155 if(uninitialized.find(identifier)!=uninitialized.end())
166 "use of uninitialized local variable");
176 for(
const auto &
object : written)
178 if(
object.
id() == ID_symbol)
219 if(f_it->second.body_available())
222 out <<
"//// Function: " << f_it->first <<
'\n';
225 uninitialized_analysis(f_it->first, f_it->second.body, ns);
226 uninitialized_analysis.
output(ns, f_it->second.body, out);
exprt guard
Guard for gotos, assume, assert.
irep_idt name
The unique identifier.
Detection for Uninitialized Local Variables.
const code_declt & to_code_decl(const codet &code)
const std::string & id2string(const irep_idt &d)
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
void set_property_class(const irep_idt &property_class)
uninitializedt(symbol_tablet &_symbol_table)
irep_idt mode
Language mode.
goto_program_instruction_typet type
What kind of instruction?
void get_tracking(goto_programt::const_targett i_it)
which variables need tracking, i.e., are uninitialized and may be read?
void set_comment(const irep_idt &comment)
symbol_tablet & symbol_table
const irep_idt & get_identifier() const
const irep_idt & get_identifier() const
irep_idt module
Name of module the symbol belongs to.
typet & type()
Return the type of the expression.
symbol_tablet symbol_table
Symbol table.
void show_uninitialized(const goto_modelt &goto_model, std::ostream &out)
This class represents an instruction in the GOTO intermediate representation.
virtual void output(const namespacet &ns, const goto_functionst &goto_functions, std::ostream &out) const
Output the abstract states for a whole program.
The Boolean constant true.
instructionst::iterator targett
A codet representing the declaration of a local variable.
API to expression classes.
std::set< irep_idt > tracking
instructionst::const_iterator const_targett
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
targett insert_after(const_targett target)
Insertion after the instruction pointed-to by the given instruction iterator target.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
void objects_read(const exprt &src, std::list< exprt > &dest)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Detection for Uninitialized Local Variables.
The Boolean constant false.
A generic container class for the GOTO intermediate representation of one function.
void add_assertions(const irep_idt &function_identifer, goto_programt &goto_program)
typet type
Type of symbol.
source_locationt location
Source code location of definition of symbol.
source_locationt source_location
The location of the instruction in the source file.
irep_idt base_name
Base (non-scoped) name.
#define Forall_goto_functions(it, functions)
void add_uninitialized_locals_assertions(goto_modelt &goto_model)
void objects_written(const exprt &src, std::list< exprt > &dest)
void set_identifier(const irep_idt &identifier)
#define Forall_goto_program_instructions(it, program)
Expression to hold a symbol (variable)
uninitialized_analysist uninitialized_analysis
#define forall_goto_functions(it, functions)
#define forall_goto_program_instructions(it, program)
goto_functionst goto_functions
GOTO functions.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
A codet representing an assignment in the program.
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.