13 #ifndef CPROVER_POINTER_ANALYSIS_VALUE_SET_FI_H 14 #define CPROVER_POINTER_ANALYSIS_VALUE_SET_FI_H 18 #include <unordered_set> 40 from_function = function_numbering.
number(
function);
41 from_target_index = inx;
46 to_function = function_numbering.
number(
function);
47 to_target_index = inx;
68 {
return offset_is_set && offset.is_zero(); }
82 void set(object_mapt &dest, object_map_dt::const_iterator it)
const 84 dest.
write()[it->first]=it->second;
87 bool insert(object_mapt &dest, object_map_dt::const_iterator it)
const 89 return insert(dest, it->first, it->second);
107 if(dest.
read().find(n)==dest.
read().end())
110 dest.
write()[n]=object;
119 if(old.
offset==
object.offset)
139 return insert(dest, object_numbering.
number(expr), object);
152 entryt(
const idt &_identifier,
const std::string _suffix):
153 identifier(_identifier),
164 typedef std::map<idt, entryt>
valuest;
170 typedef std::unordered_map<idt, entryt, string_hash>
valuest;
179 std::list<exprt> &dest,
183 const idt &identifier,
184 const std::string &suffix);
196 void add_var(
const idt &
id,
const std::string &suffix)
215 std::pair<valuest::iterator, bool>
r=
216 values.insert(std::pair<idt, entryt>(index, e));
218 return r.first->second;
223 for(std::list<entryt>::const_iterator
232 std::ostream &out)
const;
239 bool make_union(object_mapt &dest,
const object_mapt &src)
const;
283 const std::string &suffix,
284 const typet &original_type,
286 gvs_recursion_sett &recursion_set)
const;
313 const object_mapt &values_rhs,
314 const std::string &suffix,
316 assign_recursion_sett &recursion_set);
327 flatten_seent&)
const;
330 #endif // CPROVER_POINTER_ANALYSIS_VALUE_SET_FI_H The type of an expression.
void output(const namespacet &ns, std::ostream &out) const
void set_from(const irep_idt &function, unsigned inx)
std::unordered_set< unsigned int > dynamic_object_id_sett
const std::string & id2string(const irep_idt &d)
std::unordered_set< idt, string_hash > recfind_recursion_sett
std::unordered_set< idt, string_hash > flatten_seent
std::unordered_set< exprt, irep_hash > expr_sett
void get_reference_set_sharing(const exprt &expr, object_mapt &dest, const namespacet &ns) const
bool insert(object_mapt &dest, const exprt &src) const
bool insert(object_mapt &dest, const exprt &expr, const objectt &object) const
void do_free(const exprt &op, const namespacet &ns)
std::unordered_map< idt, entryt, string_hash > valuest
exprt to_expr(object_map_dt::const_iterator it) const
void add_var(const entryt &e)
bool insert(object_mapt &dest, const exprt &src, const mp_integer &offset) const
static const object_map_dt blank
void get_reference_set_sharing_rec(const exprt &expr, object_mapt &dest, const namespacet &ns) const
void get_value_set_rec(const exprt &expr, object_mapt &dest, const std::string &suffix, const typet &original_type, const namespacet &ns, gvs_recursion_sett &recursion_set) const
void apply_code(const exprt &code, const namespacet &ns)
std::unordered_set< idt, string_hash > gvs_recursion_sett
void set_to(const irep_idt &function, unsigned inx)
bool make_union(object_mapt &dest, const object_mapt &src) const
void flatten_rec(const entryt &, object_mapt &, flatten_seent &) const
bool insert(object_mapt &dest, unsigned n, const objectt &object) const
void get_reference_set(const exprt &expr, expr_sett &expr_set, const namespacet &ns) const
static object_numberingt object_numbering
entryt & get_entry(const entryt &e)
void assign_rec(const exprt &lhs, const object_mapt &values_rhs, const std::string &suffix, const namespacet &ns, assign_recursion_sett &recursion_set)
entryt & get_entry(const idt &id, const std::string &suffix)
void do_function_call(const irep_idt &function, const exprt::operandst &arguments, const namespacet &ns)
bool make_union(const value_set_fit &new_values)
void get_value_set(const exprt &expr, std::list< exprt > &dest, const namespacet &ns) const
objectt(const mp_integer &_offset)
void flatten(const entryt &e, object_mapt &dest) const
std::vector< exprt > operandst
void do_end_function(const exprt &lhs, const namespacet &ns)
std::unordered_set< idt, string_hash > assign_recursion_sett
void get_reference_set_sharing(const exprt &expr, expr_sett &expr_set, const namespacet &ns) const
Base class for all expressions.
void dereference_rec(const exprt &src, exprt &dest) const
static hash_numbering< irep_idt, irep_id_hash > function_numbering
reference_counting< object_map_dt > object_mapt
void assign(const exprt &lhs, const exprt &rhs, const namespacet &ns)
void add_var(const idt &id, const std::string &suffix)
bool offset_is_zero() const
bool insert(object_mapt &dest, object_map_dt::const_iterator it) const
entryt(const idt &_identifier, const std::string _suffix)
number_type number(const T &a)
void add_vars(const std::list< entryt > &vars)
unsigned from_target_index