Go to the documentation of this file.
31 if(expr.
id()==ID_symbol)
33 if(expr.
get_bool(ID_C_invalid_object))
38 const irep_idt &failed_symbol = ptr_symbol.
type.
get(ID_C_failed_symbol);
40 if(failed_symbol.
empty())
43 return !
ns.
lookup(failed_symbol, symbol);
55 if(symbol.
type.
id()==ID_code)
62 return valid_local_variables->find(symbol.
name)!=
63 valid_local_variables->end();
71 const std::string &property,
72 const std::string &msg,
91 t->guard.swap(guard_expr);
94 t->source_location.set_comment(
"dereference failure: "+msg);
112 if(expr.
id()==ID_and || expr.
id()==ID_or)
115 throw expr.
id_string()+
" must be Boolean, but got "+
123 throw expr.
id_string()+
" takes Boolean operands only, but got "+
135 guard.
swap(old_guard);
139 else if(expr.
id()==ID_if)
142 throw "if takes three arguments";
147 "first argument of if must be boolean, but got "
162 guard.
swap(old_guard);
170 guard.
swap(old_guard);
176 if(expr.
id()==ID_address_of ||
177 expr.
id()==
"reference_to")
184 if(expr.
op0().
id()==ID_dereference)
191 if(tmp.type()!=expr.
type())
192 tmp.make_typecast(expr.
type());
201 if(expr.
id()==ID_dereference)
204 throw "dereference expects one operand";
209 expr.
op0(), guard, mode);
213 else if(expr.
id()==ID_index)
218 throw "index expects two operands";
252 const bool checks_only,
270 for(goto_programt::instructionst::iterator
294 for(goto_functionst::function_mapt::iterator
311 valid_local_variables=&target->local_variables;
320 throw "assignment expects two operands";
353 if(statement==ID_expression)
356 throw "expression expects one operand";
361 else if(statement==ID_printf)
377 valid_local_variables=&target->local_variables;
410 goto_program_dereference(ns, symbol_table, options, value_sets);
427 goto_program_dereference(
443 goto_program_dereference(ns, symbol_table, options, value_sets);
456 goto_program_dereference(ns, symbol_table, options, value_sets);
471 goto_program_dereference(ns, new_symbol_table, options, value_sets);
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
bool has_subexpr(const exprt &expr, const std::function< bool(const exprt &)> &pred)
returns true if the expression has a subexpression that satisfies pred
#define Forall_operands(it, expr)
std::set< exprt > assertions
Unused.
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
typet type
Type of symbol.
void add(const exprt &expr)
virtual bool is_valid_object(const irep_idt &identifier)
Base class for all expressions.
virtual exprt dereference(const exprt &pointer, const guardt &guard, const modet mode)
Dereference the given pointer-expression.
virtual void get_values(goto_programt::const_targett l, const exprt &expr, valuest &dest)=0
bool is_true() const
Return whether the expression is a constant representing true.
function_mapt function_map
bool has_failed_symbol(const exprt &expr, const symbolt *&symbol) override
void pointer_checks(goto_programt &goto_program, symbol_tablet &symbol_table, const optionst &options, value_setst &value_sets)
value_set_dereferencet dereference
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
targett add_instruction()
Adds an instruction at the end.
typet & type()
Return the type of the expression.
void dereference_expression(goto_programt::const_targett target, exprt &expr)
Set the current target to target and remove derefence from expr.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
codet representation of a function call statement.
bool get_bool(const irep_namet &name) const
std::list< exprt > valuest
void dereference(goto_programt::const_targett target, exprt &expr, const namespacet &ns, value_setst &value_sets)
Remove dereferences in expr using value_sets to determine to what objects the pointers may be pointin...
source_locationt dereference_location
Unused.
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Wrapper for functions removing dereferences in expressions contained in a goto program.
const std::string & id_string() const
bool simplify(exprt &expr, const namespacet &ns)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const irep_idt & id() const
const code_function_callt & to_code_function_call(const codet &code)
void pointer_checks(goto_programt &goto_program)
Throw an exception in case removing dereferences from the program would throw an exception.
#define Forall_goto_functions(it, functions)
void clear()
Clear the goto program.
goto_program_instruction_typet
The type of an instruction in a GOTO program.
void get_value_set(const exprt &expr, value_setst::valuest &dest) override
Gets the value set corresponding to the current target and expression expr.
instructionst instructions
The list of instructions in the goto program.
Deprecated expression utility functions.
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_functionst goto_functions
GOTO functions.
const irep_idt & get(const irep_namet &name) const
void dereference_expr(exprt &expr, const bool checks_only, const value_set_dereferencet::modet mode)
Remove dereference expressions contained in expr.
bool get_bool_option(const std::string &option) const
exprt guard
Guard for gotos, assume, assert.
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 insert_before_swap(targett target)
Insertion that preserves jumps to "target".
void remove_pointers(goto_programt &goto_program, symbol_tablet &symbol_table, value_setst &value_sets)
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...
bool is_function_call() const
bool is_boolean() const
Return whether the expression represents a Boolean.
This class represents an instruction in the GOTO intermediate representation.
symbol_tablet symbol_table
Symbol table.
irep_idt name
The unique identifier.
instructionst::iterator targett
void set_property_class(const irep_idt &property_class)