12#ifndef CPROVER_ANALYSES_LOCAL_BITVECTOR_ANALYSIS_H
13#define CPROVER_ANALYSES_LOCAL_BITVECTOR_ANALYSIS_H
30 :
dirty(_goto_function),
32 cfg(_goto_function.body),
165 void print(std::ostream &)
const;
Dirty variables are ones which have their address taken so we can't reliably work out where they may ...
Base class for all expressions.
::goto_functiont goto_functiont
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
instructionst::const_iterator const_targett
std::vector< points_tot > loc_infost
expanding_vectort< flagst > points_tot
static bool merge(points_tot &a, points_tot &b)
goto_functionst::goto_functiont goto_functiont
local_bitvector_analysist(const goto_functiont &_goto_function, const namespacet &ns)
flagst get(const goto_programt::const_targett t, const exprt &src)
void output(std::ostream &out, const goto_functiont &goto_function, const namespacet &ns) const
flagst get_rec(const exprt &rhs, points_tot &loc_info_src)
void assign_lhs(const exprt &lhs, const exprt &rhs, points_tot &loc_info_src, points_tot &loc_info_dest)
bool is_tracked(const irep_idt &identifier)
numberingt< irep_idt > pointers
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Variables whose address is taken.
std::ostream & operator<<(std::ostream &out, const local_bitvector_analysist::flagst &flags)
Local variables whose address is taken.
static flagst mk_uses_offset()
static flagst mk_integer_address()
static flagst mk_dynamic_heap()
flagst operator|(const flagst other) const
static flagst mk_static_lifetime()
static flagst mk_unknown()
static flagst mk_dynamic_local()
bool is_static_lifetime() const
bool is_dynamic_local() const
void print(std::ostream &) const
bool is_dynamic_heap() const
bool is_uses_offset() const
bool is_uninitialized() const
bool merge(const flagst &other)
bool is_integer_address() const
static flagst mk_uninitialized()
flagst(const bitst _bits)