26 if(expr.
id()==ID_symbol)
34 ptr_symbol.
type.
get(
"#failed_symbol");
36 if(failed_symbol.
empty())
39 return !
ns.
lookup(failed_symbol, symbol);
50 if(symbol.
type.
id()==ID_code)
57 if(valid_local_variables->find(symbol.
name)!=
58 valid_local_variables->end())
68 const std::string &property,
69 const std::string &msg,
88 t->guard.swap(guard_expr);
91 t->source_location.set_comment(
"dereference failure: "+msg);
104 if(expr.
id()==ID_and || expr.
id()==ID_or)
107 throw expr.
id_string()+
" must be Boolean, but got "+
115 throw expr.
id_string()+
" takes Boolean operands only, but got "+
131 guard.
swap(old_guard);
135 else if(expr.
id()==ID_if)
138 throw "if takes three arguments";
143 "first argument of if must be boolean, but got " 158 guard.
swap(old_guard);
168 guard.
swap(old_guard);
174 if(expr.
id()==ID_address_of ||
175 expr.
id()==
"reference_to")
182 if(expr.
op0().
id()==ID_dereference)
189 if(tmp.type()!=expr.
type())
190 tmp.make_typecast(expr.
type());
199 if(expr.
id()==ID_dereference)
202 throw "dereference expects one operand";
207 expr.
op0(), guard, mode);
211 else if(expr.
id()==ID_index)
216 throw "index expects two operands";
240 const bool checks_only,
258 for(goto_programt::instructionst::iterator
282 for(goto_functionst::function_mapt::iterator
295 valid_local_variables=&target->local_variables;
304 throw "assignment expects two operands";
337 if(statement==ID_expression)
340 throw "expression expects one operand";
345 else if(statement==ID_printf)
360 valid_local_variables=&target->local_variables;
388 goto_program_dereference(ns, symbol_table, options, value_sets);
402 goto_program_dereference(
417 goto_program_dereference(ns, symbol_table, options, value_sets);
429 goto_program_dereference(ns, symbol_table, options, value_sets);
442 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
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)
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)
Deprecated expression utility functions.
source_locationt dereference_location
goto_programt::const_targett current_target
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
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)
bool get_bool(const irep_namet &name) const
This class represents an instruction in the GOTO intermediate representation.
void clear()
Clear the goto program.
virtual void get_value_set(const exprt &expr, value_setst::valuest &dest)
void pointer_checks(goto_programt &goto_program)
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
instructionst instructions
The list of instructions in the goto program.
bool get_bool_option(const std::string &option) const
const irep_idt & get(const irep_namet &name) const
instructionst::const_iterator const_targett
goto_program_instruction_typet
The type of an instruction in a GOTO program.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
virtual void dereference_failure(const std::string &property, const std::string &msg, const guardt &guard)
A generic container class for the GOTO intermediate representation of one function.
typet type
Type of symbol.
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)
targett add_instruction()
Adds an instruction at the end.
Base class for all expressions.
virtual bool has_failed_symbol(const exprt &expr, const symbolt *&symbol)
#define Forall_goto_functions(it, functions)
void dereference_instruction(goto_programt::targett target, bool checks_only=false)
const std::string & id_string() const
#define Forall_operands(it, expr)
goto_programt & goto_program
const codet & to_code(const exprt &expr)
std::list< exprt > valuest
goto_functionst goto_functions
GOTO functions.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See 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)