25 if(expr.
id()==ID_symbol)
33 ptr_symbol.
type.
get(
"#failed_symbol");
35 if(failed_symbol.
empty())
38 return !
ns.
lookup(failed_symbol, symbol);
49 if(symbol.
type.
id()==ID_code)
67 const std::string &property,
68 const std::string &msg,
87 t->guard.swap(guard_expr);
90 t->source_location.set_comment(
"dereference failure: "+msg);
103 if(expr.
id()==ID_and || expr.
id()==ID_or)
106 throw expr.
id_string()+
" must be Boolean, but got "+
111 for(
unsigned i=0; i<expr.
operands().size(); i++)
116 throw expr.
id_string()+
" takes Boolean operands only, but got "+
132 guard.
swap(old_guard);
136 else if(expr.
id()==ID_if)
139 throw "if takes three arguments";
144 "first argument of if must be boolean, but got " 159 guard.
swap(old_guard);
169 guard.
swap(old_guard);
175 if(expr.
id()==ID_address_of ||
176 expr.
id()==
"reference_to")
183 if(expr.
op0().
id()==ID_dereference)
190 if(tmp.type()!=expr.
type())
191 tmp.make_typecast(expr.
type());
200 if(expr.
id()==ID_dereference)
203 throw "dereference expects one operand";
208 expr.
op0(), guard, mode);
212 else if(expr.
id()==ID_index)
217 throw "index expects two operands";
241 const bool checks_only,
259 for(goto_programt::instructionst::iterator
283 for(goto_functionst::function_mapt::iterator
298 goto_programt::instructiont &i=*target;
304 if(i.code.operands().size()!=2)
305 throw "assignment expects two operands";
312 else if(i.is_function_call())
329 else if(i.is_return())
334 else if(i.is_other())
336 const irep_idt &statement=i.code.get(ID_statement);
338 if(statement==ID_expression)
340 if(i.code.operands().size()!=1)
341 throw "expression expects one operand";
346 else if(statement==ID_printf)
389 goto_program_dereference(ns, symbol_table, options, value_sets);
404 goto_program_dereference(ns, symbol_table, options, value_sets);
418 goto_program_dereference(ns, symbol_table, options, value_sets);
430 goto_program_dereference(ns, symbol_table, options, value_sets);
443 goto_program_dereference(ns, new_symbol_table, options, value_sets);
irep_idt name
The unique identifier.
goto_program_instruction_typet
The type of an instruction in a GOTO program.
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
std::set< exprt > assertions
targett add_instruction()
Adds an instruction at the end.
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 clear()
Clear the goto program.
void remove_pointers(goto_programt &goto_program, symbol_tablet &symbol_table, value_setst &value_sets)
virtual bool is_valid_object(const irep_idt &identifier)
virtual exprt dereference(const exprt &pointer, const guardt &guard, const modet mode)
instructionst instructions
The list of instructions in the goto program.
source_locationt dereference_location
goto_programt::const_targett current_target
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
virtual void get_value_set(const exprt &expr, value_setst::valuest &dest)
void pointer_checks(goto_programt &goto_program)
const irep_idt & id() const
instructionst::const_iterator const_targett
void pointer_checks(goto_programt &goto_program, symbol_tablet &symbol_table, const optionst &options, value_setst &value_sets)
const std::set< irep_idt > * valid_local_variables
const source_locationt & find_source_location() const
bool get_bool_option(const std::string &option) const
const irep_idt & get(const irep_namet &name) const
virtual void dereference_failure(const std::string &property, const std::string &msg, const guardt &guard)
function_mapt function_map
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
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)
Base class for all expressions.
virtual bool has_failed_symbol(const exprt &expr, const symbolt *&symbol)
#define Forall_goto_functions(it, functions)
static bool has_dereference(const exprt &expr)
Returns 'true' iff the given expression contains unary '*'.
void dereference_instruction(goto_programt::targett target, bool checks_only=false)
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
const std::string & id_string() const
#define Forall_operands(it, expr)
const codet & to_code(const exprt &expr)
std::list< exprt > valuest
void add(const exprt &expr)
const code_function_callt & to_code_function_call(const codet &code)
bool simplify(exprt &expr, const namespacet &ns)
instructionst::iterator targett