12 #ifndef CPROVER_ANALYSES_LOCAL_BITVECTOR_ANALYSIS_H 13 #define CPROVER_ANALYSES_LOCAL_BITVECTOR_ANALYSIS_H 29 const goto_functiont &_goto_function):
30 dirty(_goto_function),
32 cfg(_goto_function.body)
34 build(_goto_function);
39 const goto_functiont &goto_function,
164 void print(std::ostream &)
const;
179 void build(
const goto_functiont &goto_function);
222 #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
void build(const goto_functiont &goto_function)
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
void assign_lhs(const exprt &lhs, const exprt &rhs, const loc_infot &loc_info_src, loc_infot &loc_info_dest)
static flagst mk_static_lifetime()
flagst operator|(const flagst other) const
static flagst mk_integer_address()
instructionst::const_iterator const_targett
bool is_integer_address() const
static flagst mk_dynamic_local()
bool is_dynamic_local() const
std::vector< loc_infot > loc_infost
void output(std::ostream &out, const goto_functiont &goto_function, const namespacet &ns) const
bool merge(const flagst &other)
goto_function_templatet< goto_programt > goto_functiont
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()
flagst get_rec(const exprt &rhs, const loc_infot &loc_info_src)
static flagst mk_uninitialized()
Local variables whose address is taken.
local_bitvector_analysist(const goto_functiont &_goto_function)
std::stack< unsigned > work_queuet