12 #ifndef CPROVER_ANALYSES_CUSTOM_BITVECTOR_ANALYSIS_H 13 #define CPROVER_ANALYSES_CUSTOM_BITVECTOR_ANALYSIS_H 58 "If the domain is bottom, it must have no bits set");
66 "If the domain is top, it must have no bits set");
77 typedef std::map<irep_idt, bit_vectort>
bitst;
139 return (src&(1ll<<bit_nr))!=0;
153 bool xml, std::ostream &);
179 #endif // CPROVER_ANALYSES_CUSTOM_BITVECTOR_ANALYSIS_H
void transform(locationt from, locationt to, ai_baset &ai, const namespacet &ns) final override
how function calls are treated: a) there is an edge from each call site to the function head b) there...
goto_programt::const_targett locationt
std::map< irep_idt, bit_vectort > bitst
bool is_bottom() const final override
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)
void make_top() final override
all states – the analysis doesn't use this, and domains may refuse to implement it...
static bool get_bit(const bit_vectort src, unsigned bit_nr)
bool is_top() const final override
void make_bottom() final override
no states
void assign_lhs(const exprt &, const vectorst &)
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const final override
void check(const goto_modelt &, bool xml, std::ostream &)
custom_bitvector_domaint & operator[](locationt l)
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
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
void make_entry() final override
a reasonable entry-point state
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
numbering< irep_idt > bitst
unsigned get_bit_nr(const exprt &)
static void set_bit(bit_vectort &dest, unsigned bit_nr)
custom_bitvector_domaint()
void instrument(goto_functionst &)
The basic interface of an abstract interpreter.
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
#define DATA_INVARIANT(CONDITION, REASON)
unsigned long long bit_vectort
static vectorst merge(const vectorst &a, const vectorst &b)
void assign_struct_rec(locationt from, const exprt &lhs, const exprt &rhs, custom_bitvector_analysist &, const namespacet &)
Field-insensitive, location-sensitive may-alias analysis.