25 #ifndef CPROVER_ANALYSES_REACHING_DEFINITIONS_H 26 #define CPROVER_ANALYSES_REACHING_DEFINITIONS_H 46 const V &
get(
const std::size_t value_index)
const 48 assert(value_index<
values.size());
49 return values[value_index]->first;
52 std::size_t
add(
const V &value)
56 std::pair<typename inner_mapt::iterator, bool> entry=
57 m.insert(std::make_pair(value,
values.size()));
60 values.push_back(entry.first);
62 return entry.first->second;
77 std::vector<typename inner_mapt::const_iterator>
values;
204 "If domain is top, the value map must be empty");
211 "If domain is bottom, the value map must be empty");
239 typedef std::multimap<range_spect, range_spect>
rangest;
265 typedef std::map<irep_idt, values_innert>
valuest;
267 typedef std::unordered_map<irep_idt, values_innert>
valuest;
333 void output(std::ostream &out)
const;
360 "rd_state has type rd_range_domaint");
392 #endif // CPROVER_ANALYSES_REACHING_DEFINITIONS_H
void kill(const irep_idt &identifier, const range_spect &range_start, const range_spect &range_end)
#define INVARIANT_STRUCTURED(CONDITION, TYPENAME,...)
void initialize(const goto_functionst &goto_functions) override
Initialize all the abstract states for a whole program.
void transform_end_function(const namespacet &ns, const irep_idt &function_from, locationt from, locationt to, reaching_definitions_analysist &rd)
virtual statet & get_state(locationt l) override
Get the state for the given location, creating it in a default way if it doesn't exist.
void clear_cache(const irep_idt &identifier) const
goto_programt::const_targett locationt
ai_domain_baset::locationt definition_at
The iterator to the GOTO instruction where the variable has been written to.
std::unordered_map< irep_idt, ranges_at_loct > export_cachet
std::unique_ptr< dirtyt > is_dirty
const dirtyt & get_is_dirty() const
bool merge_inner(values_innert &dest, const values_innert &other)
Identifies a GOTO instruction where a given variable is defined (i.e.
range_spect bit_begin
The two integers below define a range of bits (i.e.
sparse_bitvector_analysist< reaching_definitiont > * bv_container
It points to the actual reaching definitions data of individual program variables.
statet & get_state(locationt l) override
Get the state for the given location, creating it in a default way if it doesn't exist.
An instance of this class provides an assignment of unique numeric ID to each inserted reaching_defin...
void transform_function_call(const namespacet &ns, const irep_idt &function_from, locationt from, const irep_idt &function_to, reaching_definitions_analysist &rd)
bool is_top() const override final
irep_idt identifier
The name of the variable which was defined.
virtual ~reaching_definitions_analysist()
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
void make_bottom() final override
no states
void kill_inf(const irep_idt &identifier, const range_spect &range_start)
void populate_cache(const irep_idt &identifier) const
Given the passed variable name identifier it collects data from bv_container for each ID in values[id...
std::unordered_map< irep_idt, values_innert > valuest
void set_bitvector_container(sparse_bitvector_analysist< reaching_definitiont > &_bv_container)
bool gen(locationt from, const irep_idt &identifier, const range_spect &range_start, const range_spect &range_end)
A utility function which updates internal data structures by inserting a new reaching definition reco...
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
std::unique_ptr< value_setst > value_sets
value_setst & get_value_sets() const
void transform_start_thread(const namespacet &ns, reaching_definitions_analysist &rd)
void output(std::ostream &out, const ai_baset &, const namespacet &) const final override
A collection of goto functions.
Because the class is inherited from ai_domain_baset, its instance represents an element of a domain o...
void transform_dead(const namespacet &ns, locationt from)
Computes an instance obtained from a *this by transformation over DEAD v GOTO instruction.
std::map< reaching_definitiont, std::size_t > inner_mapt
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
bool merge_shared(const rd_range_domaint &other, locationt from, locationt to, const namespacet &ns)
tvt has_values
This (three value logic) flag determines, whether the instance represents top, bottom, or any other element of the lattice, by values TRUE, FALSE, and UNKNOWN respectively.
valuest values
It is an ordered map from program variable names to IDs of reaching_definitiont instances stored in m...
bool operator<(const reaching_definitiont &a, const reaching_definitiont &b)
In order to use instances of this structure as keys in ordered containers, such as std::map...
std::vector< typename inner_mapt::const_iterator > values
It is a map from an ID to the corresponding reaching_definitiont instance inside the map value_map...
bool is_bottom() const override final
bool merge(const rd_range_domaint &other, locationt from, locationt to)
Implements the join operation of two instances *this and other`.
The basic interface of an abstract interpreter.
void transform(const irep_idt &function_from, locationt from, const irep_idt &function_to, locationt to, ai_baset &ai, const namespacet &ns) final override
Computes an instance obtained from the instance *this by transformation over a GOTO instruction refer...
export_cachet export_cache
It is a helper data structure.
void make_top() final override
all states – the analysis doesn't use this, and domains may refuse to implement it...
reaching_definitions_analysist(const namespacet &_ns)
std::size_t add(const V &value)
goto_programt::const_targett locationt
std::multimap< range_spect, range_spect > rangest
void transform_assign(const namespacet &ns, locationt from, locationt to, reaching_definitions_analysist &rd)
std::unordered_map< irep_idt, inner_mapt > value_map
A map from names of program variables to a set of pairs (reaching_definitiont, ID).
std::unique_ptr< is_threadedt > is_threaded
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions, goto_programs, exprts, etc.
void make_entry() final override
Make this domain a reasonable entry-point state.
std::map< locationt, rangest > ranges_at_loct
Generic exception types primarily designed for use with invariants.
std::set< std::size_t > values_innert
const is_threadedt & get_is_threaded() const