12 #ifndef CPROVER_ANALYSES_CUSTOM_BITVECTOR_ANALYSIS_H 13 #define CPROVER_ANALYSES_CUSTOM_BITVECTOR_ANALYSIS_H 62 "If the domain is bottom, it must have no bits set");
70 "If the domain is top, it must have no bits set");
81 typedef std::map<irep_idt, bit_vectort>
bitst;
143 return (src&(1ll<<bit_nr))!=0;
157 bool xml, std::ostream &);
183 #endif // CPROVER_ANALYSES_CUSTOM_BITVECTOR_ANALYSIS_H
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)
Initialize all the abstract states for a whole program.
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 &)
virtual void initialize(const goto_programt &goto_program)
Initialize all the abstract states for a single function.
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
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
void make_entry() final override
Make this domain a reasonable entry-point state.
void transform(const irep_idt &function_from, locationt from, const irep_idt &function_to, 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...
A collection of goto functions.
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)
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)
This condition should be used to document that assumptions that are made on goto_functions, goto_programs, exprts, etc.
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.