12 #ifndef CPROVER_POINTER_ANALYSIS_VALUE_SET_DEREFERENCE_H 13 #define CPROVER_POINTER_ANALYSIS_VALUE_SET_DEREFERENCE_H 15 #include <unordered_set> 49 bool _exclude_null_derefs):
81 typedef std::unordered_set<exprt, irep_hash>
expr_sett;
97 const typet &object_type,
98 const typet &dereference_type)
const;
102 const exprt &offset)
const;
139 const exprt &pointer,
144 const exprt &premise,
158 const exprt &offset);
164 const exprt &offset);
170 const exprt &offset);
173 #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)
value_set_dereferencet(const namespacet &_ns, symbol_tablet &_new_symbol_table, const optionst &_options, dereference_callbackt &_dereference_callback, const irep_idt _language_mode, bool _exclude_null_derefs)
Constructor.
API to expression classes.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
valuet build_reference_to(const exprt &what, const modet mode, const exprt &pointer, const guardt &guard)
Get a guard and expression to access what under guard.
The boolean constant false.
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)
const bool exclude_null_derefs
Flag indicating whether value_set_dereferencet::dereference should disregard an apparent attempt to d...
bool dereference_type_compare(const typet &object_type, const typet &dereference_type) const
std::unordered_set< exprt, irep_hash > expr_sett
Return value for build_reference_to; see that method for documentation.