12 #ifndef CPROVER_POINTER_ANALYSIS_GOTO_PROGRAM_DEREFERENCE_H 13 #define CPROVER_POINTER_ANALYSIS_GOTO_PROGRAM_DEREFERENCE_H 37 dereference(_ns, _new_symbol_table, _options, *this, ID_nil, false)
43 bool checks_only=
false);
47 bool checks_only=
false);
73 const std::string &property,
74 const std::string &msg,
81 bool checks_only=
false);
88 const bool checks_only,
92 const std::set<irep_idt> *valid_local_variables;
128 #endif // CPROVER_POINTER_ANALYSIS_GOTO_PROGRAM_DEREFERENCE_H std::set< exprt > assertions
virtual bool is_valid_object(const irep_idt &identifier)
source_locationt dereference_location
goto_programt::const_targett current_target
goto_program_dereferencet(const namespacet &_ns, symbol_tablet &_new_symbol_table, const optionst &_options, value_setst &_value_sets)
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
void dereference_rec(exprt &expr, guardt &guard, const value_set_dereferencet::modet mode)
void remove_pointers(goto_modelt &, value_setst &)
virtual void get_value_set(const exprt &expr, value_setst::valuest &dest)
void pointer_checks(goto_programt &goto_program)
instructionst::iterator targett
instructionst::const_iterator const_targett
virtual void dereference_failure(const std::string &property, const std::string &msg, const guardt &guard)
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
A generic container class for the GOTO intermediate representation of one function.
void dereference_expr(exprt &expr, const bool checks_only, const value_set_dereferencet::modet mode)
void dereference_expression(goto_programt::const_targett target, exprt &expr)
value_set_dereferencet dereference
void dereference_program(goto_programt &goto_program, bool checks_only=false)
Base class for all expressions.
virtual bool has_failed_symbol(const exprt &expr, const symbolt *&symbol)
void dereference_instruction(goto_programt::targett target, bool checks_only=false)
goto_programt & goto_program
virtual ~goto_program_dereferencet()
std::list< exprt > valuest
void pointer_checks(goto_programt &, symbol_tablet &, const optionst &, value_setst &)
void dereference(goto_programt::const_targett target, exprt &expr, const namespacet &, value_setst &)