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;
63 std::unordered_map<irep_idt, inner_mapt, irep_id_hash>
value_map;
164 typedef std::multimap<range_spect, range_spect>
rangest;
180 typedef std::map<irep_idt, values_innert>
valuest;
182 typedef std::unordered_map<irep_idt, values_innert, irep_id_hash>
valuest;
189 typedef std::unordered_map<irep_idt, ranges_at_loct, irep_id_hash>
231 void output(std::ostream &out)
const;
266 "rd_state has type rd_range_domaint");
298 #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,...)
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, values_innert, irep_id_hash > valuest
void transform(locationt from, locationt to, ai_baset &ai, const namespacet &ns) final
const dirtyt & get_is_dirty() const
bool merge_inner(values_innert &dest, const values_innert &other)
sparse_bitvector_analysist< reaching_definitiont > * bv_container
std::unordered_map< irep_idt, inner_mapt, irep_id_hash > value_map
instructionst::const_iterator const_targett
virtual ~reaching_definitions_analysist()
void kill_inf(const irep_idt &identifier, const range_spect &range_start)
void populate_cache(const irep_idt &identifier) const
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)
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::unordered_map< irep_idt, ranges_at_loct, irep_id_hash > export_cachet
virtual void initialize(const goto_functionst &goto_functions)
std::vector< typename inner_mapt::const_iterator > values
bool merge(const rd_range_domaint &other, locationt from, locationt to)
virtual statet & get_state(goto_programt::const_targett l)
is_threadedt * is_threaded
export_cachet export_cache
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::map< locationt, rangest > ranges_at_loct
Generic exception types primarily designed for use with invariants.
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const final
std::set< std::size_t > values_innert
const is_threadedt & get_is_threaded() const