cprover
|
#include <goto_program_dereference.h>
Public Member Functions | |
goto_program_dereferencet (const namespacet &_ns, symbol_tablet &_new_symbol_table, const optionst &_options, value_setst &_value_sets) | |
void | dereference_program (goto_programt &goto_program, bool checks_only=false) |
void | dereference_program (goto_functionst &goto_functions, bool checks_only=false) |
void | pointer_checks (goto_programt &goto_program) |
void | pointer_checks (goto_functionst &goto_functions) |
void | dereference_expression (goto_programt::const_targett target, exprt &expr) |
virtual | ~goto_program_dereferencet () |
Protected Member Functions | |
virtual bool | is_valid_object (const irep_idt &identifier) |
virtual bool | has_failed_symbol (const exprt &expr, const symbolt *&symbol) |
virtual void | dereference_failure (const std::string &property, const std::string &msg, const guardt &guard) |
virtual void | get_value_set (const exprt &expr, value_setst::valuest &dest) |
void | dereference_instruction (goto_programt::targett target, bool checks_only=false) |
void | dereference_rec (exprt &expr, guardt &guard, const value_set_dereferencet::modet mode) |
void | dereference_expr (exprt &expr, const bool checks_only, const value_set_dereferencet::modet mode) |
![]() | |
virtual | ~dereference_callbackt () |
Protected Attributes | |
const optionst & | options |
const namespacet & | ns |
value_setst & | value_sets |
value_set_dereferencet | dereference |
source_locationt | dereference_location |
goto_programt::const_targett | current_target |
std::set< exprt > | assertions |
goto_programt | new_code |
Definition at line 22 of file goto_program_dereference.h.
|
inline |
Definition at line 29 of file goto_program_dereference.h.
|
inlinevirtual |
Definition at line 54 of file goto_program_dereference.h.
|
protected |
Definition at line 238 of file goto_program_dereference.cpp.
References dereference_rec().
Referenced by dereference_expression(), and dereference_instruction().
void goto_program_dereferencet::dereference_expression | ( | goto_programt::const_targett | target, |
exprt & | expr | ||
) |
Definition at line 354 of file goto_program_dereference.cpp.
References current_target, dereference_expr(), and value_set_dereferencet::READ.
Referenced by dereference().
|
protectedvirtual |
Implements dereference_callbackt.
Definition at line 67 of file goto_program_dereference.cpp.
References goto_programt::add_instruction(), guardt::as_expr(), ASSERT, assertions, ASSUME, dereference_location, optionst::get_bool_option(), exprt::is_true(), exprt::make_not(), new_code, ns, options, source_locationt::set_property_class(), and simplify().
|
protected |
Definition at line 289 of file goto_program_dereference.cpp.
References goto_programt::instructiont::code, current_target, dereference_expr(), Forall_operands, code_function_callt::function(), irept::get(), goto_programt::instructiont::guard, goto_programt::instructiont::is_assign(), goto_programt::instructiont::is_function_call(), irept::is_not_nil(), goto_programt::instructiont::is_other(), goto_programt::instructiont::is_return(), code_function_callt::lhs(), exprt::op0(), exprt::op1(), exprt::op2(), exprt::operands(), value_set_dereferencet::READ, to_code(), to_code_function_call(), and value_set_dereferencet::WRITE.
Referenced by dereference_program().
void goto_program_dereferencet::dereference_program | ( | goto_programt & | goto_program, |
bool | checks_only = false |
||
) |
Definition at line 254 of file goto_program_dereference.cpp.
References assertions, goto_programt::clear(), dereference_instruction(), goto_program, goto_programt::insert_before_swap(), goto_programt::instructions, and new_code.
Referenced by dereference_program(), pointer_checks(), and remove_pointers().
void goto_program_dereferencet::dereference_program | ( | goto_functionst & | goto_functions, |
bool | checks_only = false |
||
) |
Definition at line 278 of file goto_program_dereference.cpp.
References dereference_program(), and goto_functionst::function_map.
|
protected |
Definition at line 96 of file goto_program_dereference.cpp.
References guardt::add(), dereference, value_set_dereferencet::dereference(), dereference_location, exprt::find_source_location(), Forall_operands, has_subexpr(), irept::id(), irept::id_string(), exprt::is_boolean(), exprt::make_not(), exprt::op0(), exprt::op1(), exprt::op2(), exprt::operands(), irept::pretty(), value_set_dereferencet::READ, irept::swap(), and exprt::type().
Referenced by dereference_expr().
|
protectedvirtual |
Implements dereference_callbackt.
Definition at line 231 of file goto_program_dereference.cpp.
References current_target, value_setst::get_values(), and value_sets.
|
protectedvirtual |
Implements dereference_callbackt.
Definition at line 22 of file goto_program_dereference.cpp.
References dstringt::empty(), irept::get(), irept::get_bool(), irept::id(), namespacet::lookup(), ns, to_symbol_expr(), and symbolt::type.
|
protectedvirtual |
Definition at line 45 of file goto_program_dereference.cpp.
References irept::id(), symbolt::is_static_lifetime, namespacet::lookup(), symbolt::name, ns, and symbolt::type.
void goto_program_dereferencet::pointer_checks | ( | goto_programt & | goto_program | ) |
Definition at line 366 of file goto_program_dereference.cpp.
References dereference_program(), and goto_program.
Referenced by pointer_checks().
void goto_program_dereferencet::pointer_checks | ( | goto_functionst & | goto_functions | ) |
Definition at line 372 of file goto_program_dereference.cpp.
References dereference_program().
|
protected |
Definition at line 95 of file goto_program_dereference.h.
Referenced by dereference_failure(), and dereference_program().
|
protected |
Definition at line 93 of file goto_program_dereference.h.
Referenced by dereference_expression(), dereference_instruction(), and get_value_set().
|
protected |
Definition at line 62 of file goto_program_dereference.h.
Referenced by dereference_rec().
|
protected |
Definition at line 92 of file goto_program_dereference.h.
Referenced by dereference_failure(), and dereference_rec().
|
protected |
Definition at line 96 of file goto_program_dereference.h.
Referenced by dereference_failure(), and dereference_program().
|
protected |
Definition at line 60 of file goto_program_dereference.h.
Referenced by dereference_failure(), has_failed_symbol(), and is_valid_object().
|
protected |
Definition at line 59 of file goto_program_dereference.h.
Referenced by dereference_failure().
|
protected |
Definition at line 61 of file goto_program_dereference.h.
Referenced by get_value_set().