12 #ifndef CPROVER_ANALYSES_CUSTOM_BITVECTOR_ANALYSIS_H 13 #define CPROVER_ANALYSES_CUSTOM_BITVECTOR_ANALYSIS_H 63 typedef std::map<irep_idt, bit_vectort>
bitst;
118 return (src&(1ll<<bit_nr))!=0;
133 bool xml, std::ostream &);
159 #endif // CPROVER_ANALYSES_CUSTOM_BITVECTOR_ANALYSIS_H
void transform(locationt from, locationt to, ai_baset &ai, const namespacet &ns) final
goto_programt::const_targett locationt
std::map< irep_idt, bit_vectort > bitst
local_may_alias_factoryt local_may_alias_factory
virtual void initialize(const goto_functionst &_goto_functions)
static irep_idt object2id(const exprt &)
xmlt xml(const source_locationt &location)
static bool get_bit(const bit_vectort src, unsigned bit_nr)
void assign_lhs(const exprt &, const vectorst &)
custom_bitvector_domaint & operator[](locationt l)
void check(const namespacet &, const goto_functionst &, bool xml, std::ostream &)
static void clear_bit(bit_vectort &dest, unsigned bit_nr)
void set_bit(const exprt &, unsigned bit_nr, modet)
void erase_blank_vectors(bitst &)
erase blank bitvectors
static bool has_get_must_or_may(const exprt &)
exprt eval(const exprt &src, custom_bitvector_analysist &) const
vectorst get_rhs(const exprt &) const
numbering< irep_idt > bitst
unsigned get_bit_nr(const exprt &)
static void set_bit(bit_vectort &dest, unsigned bit_nr)
custom_bitvector_domaint()
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const final
void instrument(goto_functionst &)
Base class for all expressions.
exprt eval(const exprt &src, locationt loc)
virtual void initialize(const goto_programt &)
bool merge(const custom_bitvector_domaint &b, locationt from, locationt to)
std::set< exprt > aliases(const exprt &, locationt loc)
goto_programt::const_targett locationt
unsigned long long bit_vectort
static vectorst merge(const vectorst &a, const vectorst &b)
Field-insensitive, location-sensitive may-alias analysis.