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;
106 bv_container(nullptr)
113 bv_container=&_bv_container;
134 bv_container->clear();
135 has_values=
tvt(
true);
142 bv_container->clear();
143 has_values=
tvt(
false);
164 typedef std::multimap<range_spect, range_spect>
rangest;
167 const ranges_at_loct &
get(
const irep_idt &identifier)
const;
170 export_cache[identifier].clear();
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>
194 void populate_cache(
const irep_idt &identifier)
const;
199 void transform_start_thread(
202 void transform_function_call(
207 void transform_end_function(
212 void transform_assign(
231 void output(std::ostream &out)
const;
235 const values_innert &other);
248 is_threaded(nullptr),
255 virtual void initialize(
266 "rd_state has type rd_range_domaint");
298 #endif // CPROVER_ANALYSES_REACHING_DEFINITIONS_H
#define INVARIANT_STRUCTURED(CONDITION, TYPENAME,...)
virtual statet & get_state(locationt l) override
void clear_cache(const irep_idt &identifier) const
ai_domain_baset::locationt definition_at
std::unordered_map< irep_idt, values_innert, irep_id_hash > valuest
const dirtyt & get_is_dirty() const
sparse_bitvector_analysist< reaching_definitiont > * bv_container
std::unordered_map< irep_idt, inner_mapt, irep_id_hash > value_map
instructionst::const_iterator const_targett
void set_bitvector_container(sparse_bitvector_analysist< reaching_definitiont > &_bv_container)
value_setst & get_value_sets() const
std::map< reaching_definitiont, std::size_t > inner_mapt
bool operator<(const reaching_definitiont &a, const reaching_definitiont &b)
std::unordered_map< irep_idt, ranges_at_loct, irep_id_hash > export_cachet
std::vector< typename inner_mapt::const_iterator > values
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
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