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)
164 void print(std::ostream &)
const;
215 #endif // CPROVER_ANALYSES_LOCAL_BITVECTOR_ANALYSIS_H
static flagst mk_unknown()
bool is_uninitialized() const
bool is_dynamic_heap() const
bool is_static_lifetime() const
Variables whose address is taken.
void print(std::ostream &) const
bool is_tracked(const irep_idt &identifier)
flagst(const bitst _bits)
goto_functionst::goto_functiont goto_functiont
flagst get_rec(const exprt &rhs, points_tot &loc_info_src)
static flagst mk_static_lifetime()
std::vector< points_tot > loc_infost
flagst operator|(const flagst other) const
static flagst mk_integer_address()
bool is_integer_address() const
static flagst mk_dynamic_local()
instructionst::const_iterator const_targett
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
bool is_dynamic_local() const
::goto_functiont goto_functiont
void output(std::ostream &out, const goto_functiont &goto_function, const namespacet &ns) const
bool merge(const flagst &other)
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
static bool merge(points_tot &a, points_tot &b)
A goto function, consisting of function type (see type), function body (see body), and parameter identifiers (see parameter_identifiers).
void assign_lhs(const exprt &lhs, const exprt &rhs, points_tot &loc_info_src, points_tot &loc_info_dest)
bool is_uses_offset() const
std::ostream & operator<<(std::ostream &out, const local_bitvector_analysist::flagst &flags)
numbering< irep_idt > pointers
Base class for all expressions.
expanding_vectort< flagst > points_tot
static flagst mk_uses_offset()
static flagst mk_dynamic_heap()
static flagst mk_uninitialized()
Local variables whose address is taken.
local_bitvector_analysist(const goto_functiont &_goto_function)
std::stack< unsigned > work_queuet