16 #ifndef CPROVER_ANALYSES_REACHING_DEFINITIONS_H 17 #define CPROVER_ANALYSES_REACHING_DEFINITIONS_H 35 const V &
get(
const std::size_t value_index)
const 37 assert(value_index<
values.size());
38 return values[value_index]->first;
41 std::size_t
add(
const V &value)
45 std::pair<typename inner_mapt::iterator, bool> entry=
46 m.insert(std::make_pair(value,
values.size()));
49 values.push_back(entry.first);
51 return entry.first->second;
62 std::vector<typename inner_mapt::const_iterator>
values;
152 "If domain is top, the value map must be empty");
159 "If domain is bottom, the value map must be empty");
176 typedef std::multimap<range_spect, range_spect>
rangest;
192 typedef std::map<irep_idt, values_innert>
valuest;
194 typedef std::unordered_map<irep_idt, values_innert>
valuest;
242 void output(std::ostream &out)
const;
270 "rd_state has type rd_range_domaint");
302 #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 transform(locationt from, locationt to, ai_baset &ai, const namespacet &ns) final override
virtual void initialize(const goto_functionst &goto_functions) override
virtual statet & get_state(locationt l) override
void clear_cache(const irep_idt &identifier) const
void transform_function_call(const namespacet &ns, locationt from, locationt to, reaching_definitions_analysist &rd)
ai_domain_baset::locationt definition_at
std::unordered_map< irep_idt, ranges_at_loct > export_cachet
std::unique_ptr< dirtyt > is_dirty
const dirtyt & get_is_dirty() const
virtual statet & get_state(goto_programt::const_targett l) override
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const final override
bool merge_inner(values_innert &dest, const values_innert &other)
sparse_bitvector_analysist< reaching_definitiont > * bv_container
bool is_top() const override final
virtual ~reaching_definitions_analysist()
void make_bottom() final override
void kill_inf(const irep_idt &identifier, const range_spect &range_start)
void populate_cache(const irep_idt &identifier) const
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)
instructionst::const_iterator const_targett
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 transform_dead(const namespacet &ns, locationt from)
std::map< reaching_definitiont, std::size_t > inner_mapt
bool merge_shared(const rd_range_domaint &other, locationt from, locationt to, const namespacet &ns)
bool operator<(const reaching_definitiont &a, const reaching_definitiont &b)
std::vector< typename inner_mapt::const_iterator > values
bool is_bottom() const override final
bool merge(const rd_range_domaint &other, locationt from, locationt to)
export_cachet export_cache
void make_top() final override
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)
void transform_end_function(const namespacet &ns, locationt from, locationt to, reaching_definitions_analysist &rd)
std::unordered_map< irep_idt, inner_mapt > value_map
std::unique_ptr< is_threadedt > is_threaded
#define DATA_INVARIANT(CONDITION, REASON)
void make_entry() final override
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