Go to the documentation of this file.
12 #ifndef CPROVER_POINTER_ANALYSIS_GOTO_PROGRAM_DEREFERENCE_H
13 #define CPROVER_POINTER_ANALYSIS_GOTO_PROGRAM_DEREFERENCE_H
39 dereference(_ns, _new_symbol_table, *this, ID_nil, false)
45 bool checks_only=
false);
49 bool checks_only=
false);
75 const std::
string &property,
76 const std::
string &msg,
83 bool checks_only=false);
90 const
bool checks_only,
94 const std::set<irep_idt> *valid_local_variables;
138 #endif // CPROVER_POINTER_ANALYSIS_GOTO_PROGRAM_DEREFERENCE_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
void pointer_checks(goto_programt &, symbol_tablet &, const optionst &, value_setst &)
void remove_pointers(goto_modelt &, value_setst &)
Remove dereferences in all expressions contained in the program goto_model.
std::set< exprt > assertions
Unused.
Base class for pointer value set analysis.
virtual bool is_valid_object(const irep_idt &identifier)
Base class for all expressions.
bool has_failed_symbol(const exprt &expr, const symbolt *&symbol) override
value_set_dereferencet dereference
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
void dereference_expression(goto_programt::const_targett target, exprt &expr)
Set the current target to target and remove derefence from expr.
void dereference(goto_programt::const_targett target, exprt &expr, const namespacet &, value_setst &)
Remove dereferences in expr using value_sets to determine to what objects the pointers may be pointin...
source_locationt dereference_location
Unused.
Wrapper for functions removing dereferences in expressions contained in a goto program.
void pointer_checks(goto_programt &goto_program)
Throw an exception in case removing dereferences from the program would throw an exception.
void get_value_set(const exprt &expr, value_setst::valuest &dest) override
Gets the value set corresponding to the current target and expression expr.
Wrapper for a function dereferencing pointer expressions using a value set.
A collection of goto functions.
void dereference_instruction(goto_programt::targett target, bool checks_only=false)
Remove dereference from expressions contained in the instruction at target.
goto_program_dereferencet(const namespacet &_ns, symbol_tablet &_new_symbol_table, const optionst &_options, value_setst &_value_sets)
void dereference_expr(exprt &expr, const bool checks_only, const value_set_dereferencet::modet mode)
Remove dereference expressions contained in expr.
void dereference_program(goto_programt &goto_program, bool checks_only=false)
goto_programt new_code
Unused.
A generic container class for the GOTO intermediate representation of one function.
instructionst::const_iterator const_targett
goto_programt::const_targett current_target
virtual void dereference_failure(const std::string &property, const std::string &msg, const guardt &guard)
void dereference_rec(exprt &expr, guardt &guard, const value_set_dereferencet::modet mode)
Turn subexpression of expr of the form &*p or reference_to(*p) to p and use dereference on subexpress...
virtual ~goto_program_dereferencet()