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 |
const std::set< irep_idt > * | valid_local_variables |
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.
References dereference_expression(), dereference_program(), and pointer_checks().
|
inlinevirtual |
Definition at line 54 of file goto_program_dereference.h.
|
protected |
Definition at line 239 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 355 of file goto_program_dereference.cpp.
References current_target, dereference_expr(), value_set_dereferencet::READ, and valid_local_variables.
Referenced by dereference(), and goto_program_dereferencet().
|
protectedvirtual |
Implements dereference_callbackt.
Definition at line 66 of file goto_program_dereference.cpp.
References goto_program_templatet< codeT, guardT >::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 290 of file goto_program_dereference.cpp.
References current_target, dereference_expr(), Forall_operands, code_function_callt::function(), irept::is_not_nil(), code_function_callt::lhs(), exprt::op2(), value_set_dereferencet::READ, to_code(), to_code_function_call(), valid_local_variables, 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 255 of file goto_program_dereference.cpp.
References assertions, goto_program_templatet< codeT, guardT >::clear(), dereference_instruction(), goto_program_templatet< codeT, guardT >::insert_before_swap(), goto_program_templatet< codeT, guardT >::instructions, and new_code.
Referenced by dereference_program(), goto_program_dereferencet(), pointer_checks(), and remove_pointers().
void goto_program_dereferencet::dereference_program | ( | goto_functionst & | goto_functions, |
bool | checks_only = false |
||
) |
Definition at line 279 of file goto_program_dereference.cpp.
References dereference_program(), and goto_functions_templatet< bodyT >::function_map.
|
protected |
Definition at line 95 of file goto_program_dereference.cpp.
References guardt::add(), dereference, value_set_dereferencet::dereference(), dereference_location, exprt::find_source_location(), Forall_operands, value_set_dereferencet::has_dereference(), 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 232 of file goto_program_dereference.cpp.
References current_target, value_setst::get_values(), and value_sets.
|
protectedvirtual |
Implements dereference_callbackt.
Definition at line 21 of file goto_program_dereference.cpp.
References dstringt::empty(), irept::get(), irept::get_bool(), irept::id(), namespacet::lookup(), ns, and symbolt::type.
|
protectedvirtual |
Definition at line 44 of file goto_program_dereference.cpp.
References irept::id(), symbolt::is_static_lifetime, namespacet::lookup(), symbolt::name, ns, symbolt::type, and valid_local_variables.
void goto_program_dereferencet::pointer_checks | ( | goto_programt & | goto_program | ) |
Definition at line 367 of file goto_program_dereference.cpp.
References dereference_program().
Referenced by goto_program_dereferencet(), and pointer_checks().
void goto_program_dereferencet::pointer_checks | ( | goto_functionst & | goto_functions | ) |
Definition at line 373 of file goto_program_dereference.cpp.
References dereference_program().
|
protected |
Definition at line 93 of file goto_program_dereference.h.
Referenced by dereference_failure(), and dereference_program().
|
protected |
Definition at line 91 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 90 of file goto_program_dereference.h.
Referenced by dereference_failure(), and dereference_rec().
|
protected |
Definition at line 94 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(), is_valid_object(), pointer_checks(), and remove_pointers().
|
protected |
Definition at line 59 of file goto_program_dereference.h.
Referenced by dereference(), dereference_failure(), and remove_pointers().
|
protected |
Definition at line 89 of file goto_program_dereference.h.
Referenced by dereference_expression(), dereference_instruction(), and is_valid_object().
|
protected |
Definition at line 61 of file goto_program_dereference.h.
Referenced by get_value_set().