Go to the documentation of this file.
12 #ifndef CPROVER_POINTER_ANALYSIS_VALUE_SET_DEREFERENCE_H
13 #define CPROVER_POINTER_ANALYSIS_VALUE_SET_DEREFERENCE_H
15 #include <unordered_set>
43 bool _exclude_null_derefs):
80 const typet &object_type,
81 const typet &dereference_type)
const;
103 const exprt &offset);
106 #endif // CPROVER_POINTER_ANALYSIS_VALUE_SET_DEREFERENCE_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Return value for build_reference_to; see that method for documentation.
The type of an expression, extends irept.
value_set_dereferencet(const namespacet &_ns, symbol_tablet &_new_symbol_table, dereference_callbackt &_dereference_callback, const irep_idt _language_mode, bool _exclude_null_derefs)
Base class for pointer value set analysis.
const irep_idt language_mode
language_mode: ID_java, ID_C or another language identifier if we know the source language in use,...
const bool exclude_null_derefs
Flag indicating whether value_set_dereferencet::dereference should disregard an apparent attempt to d...
Base class for all expressions.
virtual exprt dereference(const exprt &pointer, const guardt &guard, const modet mode)
Dereference the given pointer-expression.
virtual ~value_set_dereferencet()
symbol_tablet & new_symbol_table
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
dereference_callbackt & dereference_callback
The Boolean constant false.
bool memory_model_bytes(exprt &value, const typet &type, const exprt &offset)
Replace value by an expression of type to_type corresponding to the value at memory address value + o...
Wrapper for a function dereferencing pointer expressions using a value set.
bool dereference_type_compare(const typet &object_type, const typet &dereference_type) const
Check if the two types have matching number of ID_pointer levels, with the dereference type eventuall...
bool memory_model(exprt &value, const typet &type, const exprt &offset)
Replace value by an expression of type to_type corresponding to the value at memory address value + o...
valuet build_reference_to(const exprt &what, const exprt &pointer)