12 #ifndef CPROVER_POINTER_ANALYSIS_GOTO_PROGRAM_DEREFERENCE_H
13 #define CPROVER_POINTER_ANALYSIS_GOTO_PROGRAM_DEREFERENCE_H
52 dereference(_ns, _new_symbol_table, *this, ID_nil, false, message_handler)
58 bool checks_only=
false);
62 bool checks_only=
false);
85 bool checks_only=
false);
106 #define OPT_REMOVE_POINTERS "(remove-pointers)"
108 #define HELP_REMOVE_POINTERS \
109 " {y--remove-pointers} \t " \
110 "converts pointer arithmetic to base+offset expressions\n"
Base class for pointer value set analysis.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
A collection of goto functions.
Wrapper for functions removing dereferences in expressions contained in a goto program.
void dereference_program(goto_programt &goto_program, bool checks_only=false)
const symbolt * get_or_create_failed_symbol(const exprt &expr) override
void dereference_expr(exprt &expr, const bool checks_only)
Remove dereference expressions contained in expr.
virtual ~goto_program_dereferencet()
value_set_dereferencet dereference
std::vector< exprt > get_value_set(const exprt &expr) const override
Gets the value set corresponding to the current target and expression expr.
void dereference_instruction(goto_programt::targett target, bool checks_only=false)
Remove dereference from expressions contained in the instruction at target.
void dereference_rec(exprt &expr)
Turn subexpression of expr of the form &*p into p and use dereference on subexpressions of the form *...
goto_programt::const_targett current_target
goto_program_dereferencet(const namespacet &_ns, symbol_table_baset &_new_symbol_table, const optionst &_options, value_setst &_value_sets, message_handlert &message_handler)
void dereference_expression(const irep_idt &function_id, goto_programt::const_targett target, exprt &expr)
Set the current target to target and remove derefence from expr.
irep_idt current_function
A generic container class for the GOTO intermediate representation of one function.
instructionst::iterator targett
instructionst::const_iterator const_targett
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
The symbol table base class interface.
Wrapper for a function dereferencing pointer expressions using a value set.
void dereference(const irep_idt &function_id, goto_programt::const_targett target, exprt &expr, const namespacet &, value_setst &, message_handlert &)
Remove dereferences in expr using value_sets to determine to what objects the pointers may be pointin...
void remove_pointers(goto_modelt &, value_setst &, message_handlert &)
Remove dereferences in all expressions contained in the program goto_model.