26 if(expr.
id()==ID_symbol)
28 if(expr.
get_bool(ID_C_invalid_object))
33 const irep_idt &failed_symbol = ptr_symbol.
type.
get(ID_C_failed_symbol);
35 if(failed_symbol.
empty())
38 return !
ns.
lookup(failed_symbol, symbol);
49 if(symbol.
type.
id()==ID_code)
56 return valid_local_variables->find(symbol.
name)!=
57 valid_local_variables->end();
64 const std::string &property,
65 const std::string &msg,
84 t->guard.swap(guard_expr);
87 t->source_location.set_comment(
"dereference failure: "+msg);
100 if(expr.
id()==ID_and || expr.
id()==ID_or)
103 throw expr.
id_string()+
" must be Boolean, but got "+
111 throw expr.
id_string()+
" takes Boolean operands only, but got "+
127 guard.
swap(old_guard);
131 else if(expr.
id()==ID_if)
134 throw "if takes three arguments";
139 "first argument of if must be boolean, but got " 154 guard.
swap(old_guard);
164 guard.
swap(old_guard);
170 if(expr.
id()==ID_address_of ||
171 expr.
id()==
"reference_to")
178 if(expr.
op0().
id()==ID_dereference)
185 if(tmp.type()!=expr.
type())
186 tmp.make_typecast(expr.
type());
195 if(expr.
id()==ID_dereference)
198 throw "dereference expects one operand";
203 expr.
op0(), guard, mode);
207 else if(expr.
id()==ID_index)
212 throw "index expects two operands";
236 const bool checks_only,
254 for(goto_programt::instructionst::iterator
278 for(goto_functionst::function_mapt::iterator
291 valid_local_variables=&target->local_variables;
300 throw "assignment expects two operands";
333 if(statement==ID_expression)
336 throw "expression expects one operand";
341 else if(statement==ID_printf)
356 valid_local_variables=&target->local_variables;
384 goto_program_dereference(ns, symbol_table, options, value_sets);
398 goto_program_dereference(
413 goto_program_dereference(ns, symbol_table, options, value_sets);
425 goto_program_dereference(ns, symbol_table, options, value_sets);
438 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)
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.
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
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)