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