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
126 i1->code_nonconst() =
code_declt(symbol_expr);
142 const std::set<irep_idt> &uninitialized=
146 for(
const auto &
object : read)
148 if(
object.
id() == ID_symbol)
152 if(uninitialized.find(identifier)!=uninitialized.end())
163 "use of uninitialized local variable");
173 for(
const auto &
object : written)
175 if(
object.
id() == ID_symbol)
204 uninitialized.
add_assertions(gf_entry.first, gf_entry.second.body);
216 if(gf_entry.second.body_available())
219 out <<
"//// Function: " << gf_entry.first <<
'\n';
222 uninitialized_analysis(gf_entry.first, gf_entry.second.body, ns);
223 uninitialized_analysis.
output(
224 ns, gf_entry.first, gf_entry.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)
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.
function_mapt function_map
Expression to hold a symbol (variable)
const symbol_exprt & decl_symbol() const
Get the declared symbol for DECL.
void get_tracking(goto_programt::const_targett i_it)
which variables need tracking, i.e., are uninitialized and may be read?
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)
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.
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.
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.
codet & code_nonconst()
Set the code represented by this instruction.
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)