cprover
|
#include <path_symex_class.h>
Public Types | |
typedef path_symex_stept | stept |
Public Member Functions | |
path_symext () | |
virtual void | operator() (path_symex_statet &state, std::list< path_symex_statet > &furter_states) |
virtual void | operator() (path_symex_statet &state) |
void | do_goto (path_symex_statet &state, bool taken) |
virtual void | do_assert_fail (path_symex_statet &state) |
Protected Member Functions | |
void | do_goto (path_symex_statet &state, std::list< path_symex_statet > &further_states) |
void | function_call (path_symex_statet &state, const code_function_callt &call, std::list< path_symex_statet > &further_states) |
void | function_call_rec (path_symex_statet &state, const code_function_callt &function_call, const exprt &function, std::list< path_symex_statet > &further_states) |
void | return_from_function (path_symex_statet &state) |
void | set_return_value (path_symex_statet &, const exprt &) |
void | symex_malloc (path_symex_statet &state, const exprt &lhs, const side_effect_exprt &code) |
void | symex_va_arg_next (path_symex_statet &state, const exprt &lhs, const side_effect_exprt &code) |
void | assign (path_symex_statet &state, const exprt &lhs, const exprt &rhs) |
void | assign (path_symex_statet &state, const code_assignt &assignment) |
void | assign_rec (path_symex_statet &state, exprt::operandst &guard, const exprt &ssa_lhs, const exprt &ssa_rhs) |
Static Protected Member Functions | |
static bool | propagate (const exprt &src) |
Definition at line 17 of file path_symex_class.h.
typedef path_symex_stept path_symext::stept |
Definition at line 45 of file path_symex_class.h.
|
inline |
Definition at line 20 of file path_symex_class.h.
References do_goto(), and operator()().
|
protected |
Definition at line 92 of file path_symex.cpp.
References assign_rec(), side_effect_exprt::get_statement(), irept::id(), id2string(), path_symex_statet::read(), path_symex_statet::read_no_propagate(), symex_malloc(), symex_va_arg_next(), and to_side_effect_expr().
Referenced by assign(), function_call(), function_call_rec(), operator()(), return_from_function(), symex_malloc(), and symex_va_arg_next().
|
inlineprotected |
Definition at line 86 of file path_symex_class.h.
References assign(), assign_rec(), code_assignt::lhs(), propagate(), and code_assignt::rhs().
|
protected |
Definition at line 347 of file path_symex.cpp.
References base_type_eq(), byte_update_id(), struct_union_typet::components(), if_exprt::cond(), conjunction(), if_exprt::false_case(), namespace_baset::follow(), forall_operands, from_integer(), var_mapt::var_infot::full_identifier, path_symex_stept::full_lhs, irept::get_bool(), member_exprt::get_component_name(), symbol_exprt::get_identifier(), path_symex_statet::get_var_state(), path_symex_stept::guard, path_symex_statet::history, irept::id(), irept::id_string(), var_mapt::var_infot::increment_ssa_counter(), index_type(), irept::is_nil(), var_mapt::ns, byte_extract_exprt::offset(), byte_update_exprt::offset(), byte_extract_exprt::op(), byte_update_exprt::op(), typecast_exprt::op(), exprt::operands(), irept::pretty(), propagate(), path_symex_statet::record_step(), irept::set(), simplify_expr(), path_symex_stept::ssa_lhs, path_symex_stept::ssa_rhs, path_symex_statet::var_statet::ssa_symbol, var_mapt::var_infot::ssa_symbol(), member_exprt::struct_op(), typet::subtype(), to_array_type(), to_byte_extract_expr(), to_if_expr(), to_member_expr(), to_struct_type(), to_symbol_expr(), to_typecast_expr(), if_exprt::true_case(), exprt::type(), path_symex_statet::var_statet::value, byte_update_exprt::value(), and path_symex_statet::var_map.
Referenced by assign().
|
inlinevirtual |
Definition at line 34 of file path_symex_class.h.
References path_symex_statet::get_instruction(), path_symex_stept::guard, path_symex_statet::history, path_symex_statet::next_pc(), path_symex_statet::read(), and path_symex_statet::record_step().
Referenced by path_symex_assert_fail().
void path_symext::do_goto | ( | path_symex_statet & | state, |
bool | taken | ||
) |
Definition at line 907 of file path_symex.cpp.
References path_symex_stept::branch, path_symex_stept::BRANCH_NOT_TAKEN, path_symex_stept::BRANCH_TAKEN, loct::branch_target, path_symex_statet::get_instruction(), path_symex_stept::guard, path_symex_statet::history, loc_reft::is_nil(), loc, path_symex_statet::locs, path_symex_statet::next_pc(), path_symex_statet::pc(), path_symex_statet::read(), path_symex_statet::record_step(), path_symex_statet::set_pc(), and path_symex_statet::unwinding_map.
Referenced by operator()(), path_symex_goto(), and path_symext().
|
protected |
Definition at line 862 of file path_symex.cpp.
References path_symex_stept::branch, path_symex_stept::BRANCH_NOT_TAKEN, path_symex_stept::BRANCH_TAKEN, loct::branch_target, path_symex_statet::get_instruction(), path_symex_stept::guard, path_symex_statet::history, loc_reft::is_nil(), loc, path_symex_statet::locs, path_symex_statet::next_pc(), path_symex_statet::pc(), path_symex_statet::read(), path_symex_statet::record_step(), path_symex_statet::set_pc(), and path_symex_statet::unwinding_map.
|
inlineprotected |
Definition at line 52 of file path_symex_class.h.
References assign(), code_function_callt::function(), function_call_rec(), path_symex_statet::read(), return_from_function(), set_return_value(), symex_malloc(), and symex_va_arg_next().
Referenced by operator()().
|
protected |
Definition at line 632 of file path_symex.cpp.
References code_function_callt::arguments(), assign(), symbolt::base_name, path_symex_statet::threadt::call_stack, if_exprt::cond(), dstringt::empty(), if_exprt::false_case(), locst::function_entryt::first_loc, locst::function_map, path_symex_statet::get_current_thread(), symbol_exprt::get_identifier(), code_typet::parametert::get_identifier(), path_symex_stept::guard, code_typet::has_ellipsis(), path_symex_statet::history, id2string(), irept::is_not_nil(), code_function_callt::lhs(), path_symex_statet::threadt::local_vars, path_symex_statet::locs, exprt::make_typecast(), symbolt::name, loc_reft::next_loc(), path_symex_statet::next_pc(), code_typet::parameters(), path_symex_statet::threadt::pc, path_symex_statet::record_step(), path_symex_statet::recursion_map, symbolt::symbol_expr(), path_symex_statet::threads, to_if_expr(), to_symbol_expr(), to_typecast_expr(), if_exprt::true_case(), symbolt::type, locst::function_entryt::type, exprt::type(), and path_symex_statet::var_map.
Referenced by function_call().
|
virtual |
Definition at line 943 of file path_symex.cpp.
References path_symex_statet::add_thread(), ASSERT, ASSIGN, assign(), ASSUME, ATOMIC_BEGIN, ATOMIC_END, loct::branch_target, CATCH, DEAD, DECL, path_symex_statet::disable_current_thread(), do_goto(), END_FUNCTION, END_THREAD, FUNCTION_CALL, function_call(), path_symex_statet::get_current_thread(), path_symex_statet::get_instruction(), codet::get_statement(), GOTO, path_symex_stept::guard, path_symex_statet::history, id2string(), path_symex_statet::inside_atomic_section, loc_reft::is_nil(), loc, path_symex_statet::threadt::local_vars, LOCATION, path_symex_statet::locs, path_symex_statet::next_pc(), OTHER, path_symex_statet::threadt::pc, path_symex_statet::pc(), path_symex_statet::read(), path_symex_statet::record_step(), RETURN, return_from_function(), set_return_value(), SKIP, START_THREAD, code_declt::symbol(), path_symex_statet::threads, THROW, to_code_assign(), to_code_decl(), and to_code_function_call().
Referenced by operator()(), and path_symext().
|
virtual |
Definition at line 1105 of file path_symex.cpp.
References operator()().
|
staticprotected |
Definition at line 33 of file path_symex.cpp.
References if_exprt::false_case(), forall_operands, irept::id(), exprt::is_constant(), typecast_exprt::op(), member_exprt::struct_op(), to_array_of_expr(), to_if_expr(), to_member_expr(), to_typecast_expr(), to_union_expr(), and if_exprt::true_case().
Referenced by assign(), and assign_rec().
|
protected |
Definition at line 815 of file path_symex.cpp.
References assign(), path_symex_statet::threadt::call_stack, path_symex_statet::disable_current_thread(), path_symex_statet::get_current_thread(), path_symex_statet::threadt::local_vars, path_symex_statet::threadt::pc, path_symex_statet::recursion_map, and path_symex_statet::threads.
Referenced by function_call(), and operator()().
|
protected |
Definition at line 850 of file path_symex.cpp.
References path_symex_statet::threadt::call_stack, path_symex_statet::get_current_thread(), and path_symex_statet::threads.
Referenced by function_call(), and operator()().
|
protected |
Definition at line 156 of file path_symex.cpp.
References index_exprt::array(), assign(), symbolt::base_name, c_sizeof_type_rec(), var_mapt::dynamic_count, irept::find(), from_integer(), irept::id(), id2string(), index_type(), exprt::is_constant(), symbolt::is_lvalue, irept::is_nil(), irept::is_not_nil(), exprt::make_typecast(), symbolt::mode, symbolt::name, var_mapt::ns, exprt::op0(), exprt::op1(), exprt::operands(), pointer_offset_size(), pointer_type(), path_symex_statet::read(), irept::set(), array_typet::size(), typet::subtype(), symbolt::symbol_expr(), to_array_type(), to_integer(), symbolt::type, exprt::type(), unsigned_char_type(), and path_symex_statet::var_map.
Referenced by assign(), and function_call().
|
protected |
Definition at line 288 of file path_symex.cpp.
References assign(), var_mapt::var_infot::full_identifier, get_old_va_symbol(), path_symex_statet::get_var_state(), has_prefix(), id2string(), irept::is_nil(), exprt::make_typecast(), var_mapt::ns, exprt::op0(), exprt::operands(), pos(), path_symex_statet::read(), safe_string2unsigned(), exprt::source_location(), path_symex_statet::var_statet::ssa_symbol, exprt::type(), path_symex_statet::var_map, and zero_initializer().
Referenced by assign(), and function_call().