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);
exprt guard
Guard for gotos, assume, assert.
irep_idt name
The unique identifier.
std::set< exprt > assertions
Unused.
bool is_boolean() const
Return whether the expression represents a Boolean.
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
virtual void get_values(goto_programt::const_targett l, const exprt &expr, valuest &dest)=0
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...
void set_property_class(const irep_idt &property_class)
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
void remove_pointers(goto_programt &goto_program, symbol_tablet &symbol_table, value_setst &value_sets)
virtual bool is_valid_object(const irep_idt &identifier)
bool is_function_call() const
virtual exprt dereference(const exprt &pointer, const guardt &guard, const modet mode)
Dereference the given pointer-expression.
Deprecated expression utility functions.
void get_value_set(const exprt &expr, value_setst::valuest &dest) override
Gets the value set corresponding to the current target and expression expr.
source_locationt dereference_location
Unused.
goto_programt::const_targett current_target
bool is_true() const
Return whether the expression is a constant representing true.
function_mapt function_map
typet & type()
Return the type of the expression.
symbol_tablet symbol_table
Symbol table.
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 get_bool(const irep_namet &name) const
This class represents an instruction in the GOTO intermediate representation.
void clear()
Clear the goto program.
void pointer_checks(goto_programt &goto_program)
Throw an exception in case removing dereferences from the program would throw an exception.
const irep_idt & id() const
void pointer_checks(goto_programt &goto_program, symbol_tablet &symbol_table, const optionst &options, value_setst &value_sets)
instructionst::iterator targett
bool has_subexpr(const exprt &expr, const std::function< bool(const exprt &)> &pred)
returns true if the expression has a subexpression that satisfies pred
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
instructionst instructions
The list of instructions in the goto program.
bool has_failed_symbol(const exprt &expr, const symbolt *&symbol) override
bool get_bool_option(const std::string &option) const
const irep_idt & get(const irep_namet &name) const
instructionst::const_iterator const_targett
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
goto_program_instruction_typet
The type of an instruction in a GOTO program.
codet representation of a function call statement.
A collection of goto functions.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
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.
Wrapper for functions removing dereferences in expressions contained in a goto program.
typet type
Type of symbol.
void dereference_expr(exprt &expr, const bool checks_only, const value_set_dereferencet::modet mode)
Remove dereference expressions contained in expr.
void dereference_expression(goto_programt::const_targett target, exprt &expr)
Set the current target to target and remove derefence from expr.
value_set_dereferencet dereference
void dereference_program(goto_programt &goto_program, bool checks_only=false)
targett add_instruction()
Adds an instruction at the end.
Base class for all expressions.
#define Forall_goto_functions(it, functions)
void dereference_instruction(goto_programt::targett target, bool checks_only=false)
Remove dereference from expressions contained in the instruction at target.
const std::string & id_string() const
#define Forall_operands(it, expr)
goto_programt new_code
Unused.
std::list< exprt > valuest
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
goto_functionst goto_functions
GOTO functions.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
void add(const exprt &expr)
const code_function_callt & to_code_function_call(const codet &code)
bool simplify(exprt &expr, const namespacet &ns)