12 #ifndef CPROVER_POINTER_ANALYSIS_VALUE_SET_DEREFERENCE_H 13 #define CPROVER_POINTER_ANALYSIS_VALUE_SET_DEREFERENCE_H 15 #include <unordered_set> 75 typedef std::unordered_set<exprt, irep_hash>
expr_sett;
88 const typet &object_type,
89 const typet &dereference_type)
const;
93 const exprt &offset)
const;
109 const exprt &pointer,
114 const exprt &premise,
128 const exprt &offset);
134 const exprt &offset);
140 const exprt &offset);
143 #endif // CPROVER_POINTER_ANALYSIS_VALUE_SET_DEREFERENCE_H The type of an expression.
static const exprt & get_symbol(const exprt &object)
virtual exprt dereference(const exprt &pointer, const guardt &guard, const modet mode)
dereference_callbackt & dereference_callback
void invalid_pointer(const exprt &expr, const guardt &guard)
bool memory_model(exprt &value, const typet &type, const guardt &guard, const exprt &offset)
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
void valid_check(const exprt &expr, const guardt &guard, const modet mode)
static unsigned invalid_counter
void bounds_check(const index_exprt &expr, const guardt &guard)
virtual ~value_set_dereferencet()
bool memory_model_bytes(exprt &value, const typet &type, const guardt &guard, const exprt &offset)
API to expression classes.
valuet build_reference_to(const exprt &what, const modet mode, const exprt &pointer, const guardt &guard)
The boolean constant false.
value_set_dereferencet(const namespacet &_ns, symbol_tablet &_new_symbol_table, const optionst &_options, dereference_callbackt &_dereference_callback, const irep_idt _language_mode)
Constructor.
Base class for all expressions.
symbol_tablet & new_symbol_table
void offset_sum(exprt &dest, const exprt &offset) const
bool get_value_guard(const exprt &symbol, const exprt &premise, exprt &value)
const irep_idt language_mode
language_mode: ID_java, ID_C or another language identifier if we know the source language in use...
bool memory_model_conversion(exprt &value, const typet &type, const guardt &guard, const exprt &offset)
bool dereference_type_compare(const typet &object_type, const typet &dereference_type) const
std::unordered_set< exprt, irep_hash > expr_sett