cprover
|
The main class for the forward symbolic simulator. More...
#include <goto_symex.h>
Public Types | |
typedef goto_symex_statet | statet |
Public Member Functions | |
goto_symext (const namespacet &_ns, symbol_tablet &_new_symbol_table, symex_targett &_target) | |
virtual | ~goto_symext () |
virtual void | operator() (const goto_functionst &goto_functions) |
symex all at once, starting from entry point More... | |
virtual void | operator() (const goto_functionst &goto_functions, const goto_programt &goto_program) |
symex starting from given goto program More... | |
virtual void | operator() (statet &state, const goto_functionst &goto_functions, const goto_programt &goto_program) |
start symex in a given state More... | |
virtual void | symex_step (const goto_functionst &goto_functions, statet &state) |
execute just one step More... | |
virtual void | symex_step_goto (statet &state, bool taken) |
Public Attributes | |
unsigned | total_vccs |
unsigned | remaining_vccs |
bool | constant_propagation |
optionst | options |
symbol_tablet & | new_symbol_table |
irep_idt | language_mode |
language_mode: ID_java, ID_C or another language identifier if we know the source language in use, irep_idt() otherwise. More... | |
Protected Types | |
typedef symex_targett::assignment_typet | assignment_typet |
Protected Member Functions | |
void | new_name (symbolt &symbol) |
void | clean_expr (exprt &expr, statet &state, bool write) |
void | replace_array_equal (exprt &expr) |
void | trigger_auto_object (const exprt &expr, statet &state) |
void | initialize_auto_object (const exprt &expr, statet &state) |
void | process_array_expr (exprt &expr) |
void | process_array_expr_rec (exprt &expr, const typet &type) const |
exprt | make_auto_object (const typet &type) |
virtual void | dereference (exprt &expr, statet &state, const bool write) |
void | dereference_rec (exprt &expr, statet &state, guardt &guard, const bool write) |
void | dereference_rec_address_of (exprt &expr, statet &state, guardt &guard) |
exprt | address_arithmetic (const exprt &expr, statet &state, guardt &guard, bool keep_array) |
Evaluate an ID_address_of expression. More... | |
virtual void | symex_transition (statet &state, goto_programt::const_targett to, bool is_backwards_goto=false) |
virtual void | symex_transition (statet &state) |
virtual void | symex_goto (statet &state) |
virtual void | symex_start_thread (statet &state) |
virtual void | symex_atomic_begin (statet &state) |
virtual void | symex_atomic_end (statet &state) |
virtual void | symex_decl (statet &state) |
virtual void | symex_decl (statet &state, const symbol_exprt &expr) |
virtual void | symex_dead (statet &state) |
virtual void | symex_other (const goto_functionst &goto_functions, statet &state) |
virtual void | vcc (const exprt &expr, const std::string &msg, statet &state) |
virtual void | symex_assume (statet &state, const exprt &cond) |
void | merge_gotos (statet &state) |
virtual void | merge_goto (const statet::goto_statet &goto_state, statet &state) |
void | merge_value_sets (const statet::goto_statet &goto_state, statet &dest) |
void | phi_function (const statet::goto_statet &goto_state, statet &state) |
virtual bool | get_unwind (const symex_targett::sourcet &source, unsigned unwind) |
virtual void | loop_bound_exceeded (statet &state, const exprt &guard) |
void | pop_frame (statet &state) |
pop one call frame More... | |
void | return_assignment (statet &state) |
virtual void | no_body (const irep_idt &identifier) |
virtual void | symex_function_call (const goto_functionst &goto_functions, statet &state, const code_function_callt &call) |
virtual void | symex_end_of_function (statet &state) |
do function call by inlining More... | |
virtual void | symex_function_call_symbol (const goto_functionst &goto_functions, statet &state, const code_function_callt &call) |
virtual void | symex_function_call_code (const goto_functionst &goto_functions, statet &state, const code_function_callt &call) |
do function call by inlining More... | |
virtual bool | get_unwind_recursion (const irep_idt &identifier, const unsigned thread_nr, unsigned unwind) |
void | parameter_assignments (const irep_idt function_identifier, const goto_functionst::goto_functiont &goto_function, statet &state, const exprt::operandst &arguments) |
void | locality (const irep_idt function_identifier, statet &state, const goto_functionst::goto_functiont &goto_function) |
preserves locality of local variables of a given function by applying L1 renaming to the local identifiers More... | |
void | add_end_of_function (exprt &code, const irep_idt &identifier) |
void | symex_throw (statet &state) |
void | symex_catch (statet &state) |
virtual void | do_simplify (exprt &expr) |
void | symex_assign_rec (statet &state, const code_assignt &code) |
virtual void | symex_assign (statet &state, const code_assignt &code) |
void | symex_assign_rec (statet &state, const exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &guard, assignment_typet assignment_type) |
void | symex_assign_symbol (statet &state, const ssa_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &guard, assignment_typet assignment_type) |
void | symex_assign_typecast (statet &state, const typecast_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &guard, assignment_typet assignment_type) |
void | symex_assign_array (statet &state, const index_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &guard, assignment_typet assignment_type) |
void | symex_assign_struct_member (statet &state, const member_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &guard, assignment_typet assignment_type) |
void | symex_assign_if (statet &state, const if_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &guard, assignment_typet assignment_type) |
void | symex_assign_byte_extract (statet &state, const byte_extract_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &guard, assignment_typet assignment_type) |
virtual void | symex_gcc_builtin_va_arg_next (statet &state, const exprt &lhs, const side_effect_exprt &code) |
virtual void | symex_malloc (statet &state, const exprt &lhs, const side_effect_exprt &code) |
virtual void | symex_cpp_delete (statet &state, const codet &code) |
virtual void | symex_cpp_new (statet &state, const exprt &lhs, const side_effect_exprt &code) |
virtual void | symex_fkt (statet &state, const code_function_callt &code) |
virtual void | symex_macro (statet &state, const code_function_callt &code) |
virtual void | symex_trace (statet &state, const code_function_callt &code) |
virtual void | symex_printf (statet &state, const exprt &lhs, const exprt &rhs) |
virtual void | symex_input (statet &state, const codet &code) |
virtual void | symex_output (statet &state, const codet &code) |
void | read (exprt &expr) |
void | replace_nondet (exprt &expr) |
void | rewrite_quantifiers (exprt &expr, statet &state) |
Static Protected Member Functions | |
static bool | is_index_member_symbol_if (const exprt &expr) |
static exprt | add_to_lhs (const exprt &lhs, const exprt &what) |
Protected Attributes | |
const namespacet & | ns |
symex_targett & | target |
unsigned | atomic_section_counter |
irep_idt | guard_identifier |
Static Protected Attributes | |
static unsigned | nondet_count =0 |
static unsigned | dynamic_counter =0 |
Friends | |
class | symex_dereference_statet |
The main class for the forward symbolic simulator.
Definition at line 41 of file goto_symex.h.
|
protected |
Definition at line 265 of file goto_symex.h.
typedef goto_symex_statet goto_symext::statet |
Definition at line 66 of file goto_symex.h.
|
inline |
Definition at line 44 of file goto_symex.h.
References options, and optionst::set_option().
|
inlinevirtual |
Definition at line 62 of file goto_symex.h.
Definition at line 97 of file symex_assign.cpp.
References irept::id(), irept::is_nil(), irept::is_not_nil(), irept::make_nil(), exprt::op0(), and exprt::operands().
Referenced by symex_assign_array(), symex_assign_byte_extract(), symex_assign_struct_member(), symex_assign_symbol(), and symex_assign_typecast().
|
protected |
Evaluate an ID_address_of expression.
Definition at line 93 of file symex_dereference.cpp.
References base_type_eq(), object_descriptor_exprt::build(), byte_extract_id(), char_type(), compute_pointer_offset(), if_exprt::cond(), dereference_rec(), do_simplify(), if_exprt::false_case(), namespace_baset::follow(), from_integer(), irept::get_bool(), ssa_exprt::get_l1_object(), irept::id(), irept::id_string(), index_type(), ns, address_of_exprt::object(), byte_extract_exprt::offset(), object_descriptor_exprt::offset(), byte_extract_exprt::op(), dereference_exprt::pointer(), pointer_type(), object_descriptor_exprt::root_object(), typet::subtype(), to_address_of_expr(), to_byte_extract_expr(), to_dereference_expr(), to_if_expr(), to_ssa_expr(), if_exprt::true_case(), and exprt::type().
Referenced by dereference_rec().
Definition at line 169 of file symex_clean_expr.cpp.
References dereference(), replace_array_equal(), and replace_nondet().
Referenced by symex_assign_rec(), symex_cpp_new(), symex_goto(), symex_other(), and symex_step().
Definition at line 344 of file symex_dereference.cpp.
References goto_symex_statet::call_stack(), dereference_rec(), goto_symex_statet::L1, ns, and goto_symex_statet::rename().
Referenced by clean_expr(), dereference_rec(), and symex_step_goto().
|
protected |
Definition at line 230 of file symex_dereference.cpp.
References typet::add_source_location(), address_arithmetic(), index_exprt::array(), base_type_eq(), dereference(), namespace_baset::follow(), Forall_operands, from_integer(), irept::id(), index_exprt::index(), index_type(), language_mode, new_symbol_table, ns, address_of_exprt::object(), typecast_exprt::op(), exprt::op0(), exprt::operands(), options, dereference_exprt::pointer(), pointer_type(), value_set_dereferencet::READ, exprt::source_location(), typet::subtype(), irept::swap(), to_address_of_expr(), to_array_type(), to_index_expr(), to_typecast_expr(), trigger_auto_object(), exprt::type(), and value_set_dereferencet::WRITE.
Referenced by address_arithmetic(), dereference(), and dereference_rec_address_of().
|
protected |
Definition at line 27 of file symex_dereference.cpp.
References dereference_rec(), irept::id(), member_exprt::struct_op(), to_if_expr(), to_index_expr(), and to_member_expr().
|
protectedvirtual |
Definition at line 19 of file goto_symex.cpp.
References optionst::get_bool_option(), ns, options, and simplify().
Referenced by address_arithmetic(), phi_function(), symex_assign_if(), symex_assign_symbol(), symex_assume(), symex_atomic_end(), symex_gcc_builtin_va_arg_next(), symex_goto(), symex_input(), symex_output(), symex_printf(), symex_step_goto(), and vcc().
|
protectedvirtual |
Reimplemented in symex_bmct.
Definition at line 412 of file symex_goto.cpp.
Referenced by symex_goto().
|
protectedvirtual |
Reimplemented in symex_bmct.
Definition at line 29 of file symex_function_call.cpp.
Referenced by symex_function_call_code().
Definition at line 37 of file auto_objects.cpp.
References struct_union_typet::components(), namespace_baset::follow(), irept::id(), make_auto_object(), ns, pointer_type(), member_exprt::set_component_name(), member_exprt::struct_op(), typet::subtype(), symex_assign_rec(), to_pointer_type(), to_struct_type(), and exprt::type().
Referenced by trigger_auto_object().
|
staticprotected |
Definition at line 67 of file symex_dereference.cpp.
References irept::id(), to_if_expr(), to_index_expr(), and to_member_expr().
|
protected |
preserves locality of local variables of a given function by applying L1 renaming to the local identifiers
Definition at line 373 of file symex_function_call.cpp.
References goto_symex_statet::renaming_levelt::current_names, get_local_identifiers(), goto_symex_statet::renaming_levelt::increase_counter(), goto_symex_statet::L0, goto_symex_statet::L1, goto_symex_statet::l1_history, goto_symex_statet::level1, goto_symex_statet::framet::local_objects, namespacet::lookup(), ns, goto_symex_statet::framet::old_level1, goto_symex_statet::rename(), goto_symex_statet::source, symex_targett::sourcet::thread_nr, goto_symex_statet::threads, and goto_symex_statet::top().
Referenced by symex_function_call_code().
Definition at line 373 of file symex_goto.cpp.
References guardt::add(), optionst::get_bool_option(), goto_symex_statet::guard, exprt::is_true(), options, symex_targett::sourcet::pc, goto_symex_statet::source, symex_assume(), and vcc().
Referenced by symex_goto().
Definition at line 19 of file auto_objects.cpp.
References symbol_tablet::add(), symbolt::base_name, dynamic_counter, id2string(), symbolt::is_lvalue, symbolt::mode, symbolt::name, new_symbol_table, and symbolt::type.
Referenced by initialize_auto_object().
|
protectedvirtual |
Reimplemented in symex_bmct.
Definition at line 234 of file symex_goto.cpp.
References goto_symex_statet::goto_statet::atomic_section_id, goto_symex_statet::atomic_section_id, goto_symex_statet::depth, goto_symex_statet::goto_statet::depth, goto_symex_statet::guard, goto_symex_statet::goto_statet::guard, merge_value_sets(), and phi_function().
Referenced by symex_bmct::merge_goto(), and merge_gotos().
|
protected |
Definition at line 210 of file symex_goto.cpp.
References goto_symex_statet::framet::goto_state_map, merge_goto(), symex_targett::sourcet::pc, goto_symex_statet::source, and goto_symex_statet::top().
Referenced by symex_step().
|
protected |
Definition at line 254 of file symex_goto.cpp.
References goto_symex_statet::guard, exprt::is_false(), value_sett::make_union(), goto_symex_statet::value_set, and goto_symex_statet::goto_statet::value_set.
Referenced by merge_goto().
|
protected |
Definition at line 47 of file symex_main.cpp.
References symbol_tablet::add(), get_new_name(), new_symbol_table, and ns.
|
inlineprotectedvirtual |
Reimplemented in symex_bmct.
Definition at line 213 of file goto_symex.h.
Referenced by symex_function_call_code().
|
virtual |
symex all at once, starting from entry point
symex from entry point
Definition at line 174 of file symex_main.cpp.
References goto_functions_templatet< goto_programt >::entry_point(), and goto_functions_templatet< bodyT >::function_map.
Referenced by operator()().
|
virtual |
symex starting from given goto program
symex starting from given program
Definition at line 165 of file symex_main.cpp.
References operator()().
|
virtual |
start symex in a given state
symex from given state
Definition at line 126 of file symex_main.cpp.
References goto_symex_statet::call_stack(), goto_symex_statet::framet::calling_location, goto_symex_statet::dirty, goto_symex_statet::framet::end_of_function, goto_program_templatet< codeT, guardT >::instructions, symex_targett::sourcet::pc, goto_symex_statet::source, goto_symex_statet::switch_to_thread(), symex_step(), goto_symex_statet::symex_target, symex_transition(), target, symex_targett::sourcet::thread_nr, goto_symex_statet::threads, and goto_symex_statet::top().
|
protected |
Definition at line 37 of file symex_function_call.cpp.
References symbolt::base_name, base_type_eq(), byte_extract_id(), dstringt::empty(), namespace_baset::follow(), from_integer(), code_typet::parametert::get_identifier(), code_typet::has_ellipsis(), irept::id(), id2string(), index_type(), irept::is_nil(), namespacet::lookup(), symbol_tablet::move(), symbolt::name, new_symbol_table, ns, code_typet::parameters(), symex_targett::sourcet::pc, irept::pretty(), goto_symex_statet::source, symbolt::symbol_expr(), symex_assign_rec(), symbolt::type, and exprt::type().
Referenced by symex_function_call_code().
|
protected |
Definition at line 267 of file symex_goto.cpp.
References guardt::as_expr(), symex_targett::assignment(), goto_symex_statet::assignment(), goto_symex_statet::atomic_section_id, goto_symex_statet::renaming_levelt::current_count(), goto_symex_statet::dirty, do_simplify(), ssa_exprt::get_original_expr(), goto_symex_statet::renaming_levelt::get_variables(), goto_symex_statet::guard, goto_symex_statet::goto_statet::guard, guard_identifier, exprt::is_false(), symbolt::is_shared(), goto_symex_statet::level2, goto_symex_statet::goto_statet::level2_current_count(), goto_symex_statet::goto_statet::level2_get_variables(), namespacet::lookup(), symbolt::name, ns, symex_targett::PHI, goto_symex_statet::propagation, goto_symex_statet::goto_statet::propagation, goto_symex_statet::record_events, ssa_exprt::set_level_2(), goto_symex_statet::source, target, symex_targett::sourcet::thread_nr, goto_symex_statet::threads, to_ssa_expr(), and goto_symex_statet::propagationt::values.
Referenced by merge_goto().
|
protected |
pop one call frame
Definition at line 321 of file symex_function_call.cpp.
References goto_symex_statet::call_stack(), goto_symex_statet::framet::calling_location, goto_symex_statet::renaming_levelt::current_names, goto_symex_statet::dirty, goto_symex_statet::level1, goto_symex_statet::level2, goto_symex_statet::framet::local_objects, goto_symex_statet::framet::old_level1, symex_targett::sourcet::pc, goto_symex_statet::pop_frame(), goto_symex_statet::level1t::restore_from(), symex_transition(), goto_symex_statet::threads, and goto_symex_statet::top().
Referenced by symex_end_of_function().
|
protected |
Definition at line 87 of file symex_clean_expr.cpp.
References index_exprt::array(), if_exprt::false_case(), Forall_operands, irept::get_bool(), ssa_exprt::get_original_expr(), irept::id(), byte_extract_exprt::op(), exprt::op0(), process_array_expr_rec(), irept::swap(), to_address_of_expr(), to_byte_extract_expr(), to_if_expr(), to_index_expr(), to_ssa_expr(), to_typecast_expr(), if_exprt::true_case(), and exprt::type().
Referenced by replace_array_equal(), and symex_other().
Definition at line 21 of file symex_clean_expr.cpp.
References index_exprt::array(), base_type_eq(), byte_extract_id(), if_exprt::false_case(), Forall_operands, from_integer(), irept::get_bool(), ssa_exprt::get_original_expr(), irept::id(), index_type(), ns, byte_extract_exprt::offset(), byte_extract_exprt::op(), exprt::op0(), irept::swap(), to_address_of_expr(), to_byte_extract_expr(), to_if_expr(), to_index_expr(), to_ssa_expr(), to_typecast_expr(), if_exprt::true_case(), and exprt::type().
Referenced by process_array_expr().
|
protected |
|
protected |
Definition at line 144 of file symex_clean_expr.cpp.
References namespace_baset::follow(), Forall_operands, irept::id(), ns, exprt::op0(), exprt::op1(), exprt::operands(), process_array_expr(), irept::swap(), and exprt::type().
Referenced by clean_expr().
|
protected |
Definition at line 25 of file goto_symex.cpp.
References Forall_operands, irept::get(), irept::id(), nondet_count, irept::set(), exprt::source_location(), irept::swap(), and exprt::type().
Referenced by clean_expr(), and symex_assign().
|
protected |
Definition at line 430 of file symex_function_call.cpp.
References guardt::as_expr(), base_type_eq(), goto_symex_statet::guard, irept::is_not_nil(), code_assignt::lhs(), symex_targett::location(), ns, exprt::op0(), symex_targett::sourcet::pc, irept::pretty(), goto_symex_statet::framet::return_value, code_assignt::rhs(), goto_symex_statet::source, symex_assign_rec(), target, to_code_return(), goto_symex_statet::top(), and exprt::type().
Referenced by symex_step().
Definition at line 109 of file symex_main.cpp.
References irept::id(), exprt::op0(), exprt::op1(), exprt::operands(), irept::swap(), symex_decl(), to_ssa_expr(), and to_symbol_expr().
Referenced by vcc().
|
protectedvirtual |
Definition at line 35 of file symex_assign.cpp.
References side_effect_exprt::get_statement(), symex_targett::HIDDEN, goto_symex_statet::framet::hidden_function, irept::id(), id2string(), code_assignt::lhs(), exprt::op0(), exprt::operands(), symex_targett::sourcet::pc, replace_nondet(), code_assignt::rhs(), goto_symex_statet::source, symex_targett::STATE, symex_assign_rec(), symex_cpp_new(), symex_gcc_builtin_va_arg_next(), symex_malloc(), symex_printf(), to_side_effect_expr(), to_symbol_expr(), and goto_symex_statet::top().
Referenced by symex_assign_rec(), and symex_other().
|
protected |
Definition at line 293 of file symex_assign.cpp.
References add_to_lhs(), index_exprt::array(), exprt::copy_to_operands(), update_exprt::designator(), namespace_baset::follow(), irept::id(), irept::id_string(), index_exprt::index(), update_exprt::new_value(), ns, update_exprt::old(), exprt::operands(), symex_assign_rec(), and exprt::type().
Referenced by symex_assign_rec().
|
protected |
Definition at line 456 of file symex_assign.cpp.
References add_to_lhs(), exprt::copy_to_operands(), irept::id(), byte_extract_exprt::offset(), byte_extract_exprt::op(), symex_assign_rec(), and exprt::type().
Referenced by symex_assign_rec().
|
protected |
Definition at line 423 of file symex_assign.cpp.
References guardt::add(), if_exprt::cond(), do_simplify(), if_exprt::false_case(), exprt::is_false(), exprt::is_true(), ns, goto_symex_statet::rename(), symex_assign_rec(), and if_exprt::true_case().
Referenced by symex_assign_rec().
|
protected |
Definition at line 23 of file symex_assign.cpp.
References clean_expr(), code_assignt::lhs(), code_assignt::rhs(), and symex_assign().
Referenced by initialize_auto_object(), parameter_assignments(), return_assignment(), symex_assign(), symex_assign_array(), symex_assign_byte_extract(), symex_assign_if(), symex_assign_rec(), symex_assign_struct_member(), symex_assign_typecast(), symex_cpp_new(), symex_function_call_code(), symex_gcc_builtin_va_arg_next(), symex_malloc(), and symex_step().
|
protected |
Definition at line 127 of file symex_assign.cpp.
References namespace_baset::follow(), irept::get_bool(), irept::id(), irept::id_string(), ns, exprt::op0(), exprt::op1(), exprt::operands(), symex_assign_array(), symex_assign_byte_extract(), symex_assign_if(), symex_assign_rec(), symex_assign_struct_member(), symex_assign_symbol(), symex_assign_typecast(), to_byte_extract_expr(), to_if_expr(), to_index_expr(), to_member_expr(), to_ssa_expr(), to_typecast_expr(), and exprt::type().
|
protected |
Definition at line 349 of file symex_assign.cpp.
References add_to_lhs(), exprt::copy_to_operands(), namespace_baset::follow(), member_exprt::get_component_name(), irept::id(), ns, update_exprt::old(), exprt::op0(), exprt::operands(), symex_assign_rec(), and exprt::type().
Referenced by symex_assign_rec().
|
protected |
Definition at line 205 of file symex_assign.cpp.
References add_to_lhs(), guardt::append(), guardt::as_expr(), symex_targett::assignment(), goto_symex_statet::assignment(), if_exprt::cond(), constant_propagation, goto_symex_statet::renaming_levelt::current_count(), do_simplify(), dstringt::empty(), if_exprt::false_case(), optionst::get_bool_option(), symbol_exprt::get_identifier(), ssa_exprt::get_level_1(), ssa_exprt::get_object_name(), ssa_exprt::get_original_expr(), goto_symex_statet::guard, symex_targett::HIDDEN, symbolt::is_auxiliary, symbolt::is_parameter, exprt::is_true(), goto_symex_statet::level2, namespacet::lookup(), ns, options, goto_symex_statet::record_events, goto_symex_statet::rename(), goto_symex_statet::source, irept::swap(), target, if_exprt::true_case(), and exprt::type().
Referenced by symex_assign_rec(), and symex_start_thread().
|
protected |
Definition at line 272 of file symex_assign.cpp.
References add_to_lhs(), exprt::make_typecast(), exprt::op0(), exprt::operands(), symex_assign_rec(), and exprt::type().
Referenced by symex_assign_rec().
Definition at line 80 of file symex_main.cpp.
References guardt::add(), guardt::as_expr(), symex_targett::assumption(), goto_symex_statet::atomic_section_id, do_simplify(), goto_symex_statet::guard, guardt::guard_expr(), exprt::is_false(), exprt::is_true(), goto_symex_statet::source, symex_atomic_end(), target, and goto_symex_statet::threads.
Referenced by loop_bound_exceeded(), symex_goto(), symex_step(), and symex_throw().
|
protectedvirtual |
Definition at line 14 of file symex_atomic_section.cpp.
References guardt::as_expr(), symex_targett::atomic_begin(), atomic_section_counter, goto_symex_statet::atomic_section_id, goto_symex_statet::guard, exprt::is_false(), symex_targett::sourcet::pc, goto_symex_statet::read_in_atomic_section, goto_symex_statet::source, target, and goto_symex_statet::written_in_atomic_section.
Referenced by symex_step().
|
protectedvirtual |
Definition at line 34 of file symex_atomic_section.cpp.
References guardt::as_expr(), symex_targett::atomic_end(), goto_symex_statet::atomic_section_id, goto_symex_statet::renaming_levelt::current_count(), do_simplify(), symbol_exprt::get_identifier(), goto_symex_statet::guard, exprt::is_false(), goto_symex_statet::level2, r, goto_symex_statet::read_in_atomic_section, ssa_exprt::set_level_2(), symex_targett::shared_read(), symex_targett::shared_write(), goto_symex_statet::source, target, and goto_symex_statet::written_in_atomic_section.
Referenced by symex_assume(), and symex_step().
|
protected |
Definition at line 14 of file symex_catch.cpp.
References goto_symex_statet::call_stack(), goto_symex_statet::framet::catch_map, symex_targett::sourcet::pc, goto_symex_statet::source, and goto_symex_statet::top().
Referenced by symex_step().
Definition at line 424 of file symex_builtin_functions.cpp.
Referenced by symex_other().
|
protectedvirtual |
Definition at line 364 of file symex_builtin_functions.cpp.
References symbol_tablet::add(), symbolt::base_name, clean_expr(), exprt::copy_to_operands(), dynamic_counter, irept::find(), from_integer(), irept::get(), irept::id(), id2string(), index_type(), symbolt::is_lvalue, symbolt::mode, symbolt::name, new_symbol_table, irept::set(), typet::subtype(), symbolt::symbol_expr(), symex_assign_rec(), symbolt::type, and exprt::type().
Referenced by symex_assign().
|
protectedvirtual |
Definition at line 21 of file symex_dead.cpp.
References value_sett::assign(), goto_symex_statet::renaming_levelt::current_names, namespace_baset::follow(), get_failed_symbol(), symbol_exprt::get_identifier(), irept::id(), goto_symex_statet::renaming_levelt::increase_counter(), irept::is_not_nil(), goto_symex_statet::L1, goto_symex_statet::level2, ns, address_of_exprt::object(), exprt::op0(), exprt::operands(), symex_targett::sourcet::pc, goto_symex_statet::propagation, goto_symex_statet::propagationt::remove(), goto_symex_statet::rename(), goto_symex_statet::source, to_code(), to_ssa_expr(), to_symbol_expr(), exprt::type(), and goto_symex_statet::value_set.
Referenced by symex_step().
|
protectedvirtual |
Definition at line 23 of file symex_decl.cpp.
References irept::id(), exprt::op0(), exprt::operands(), symex_targett::sourcet::pc, goto_symex_statet::source, to_code(), and to_symbol_expr().
Referenced by rewrite_quantifiers(), and symex_step().
|
protectedvirtual |
Definition at line 41 of file symex_decl.cpp.
References guardt::as_expr(), value_sett::assign(), goto_symex_statet::atomic_section_id, goto_symex_statet::renaming_levelt::current_names, symex_targett::decl(), goto_symex_statet::dirty, namespace_baset::follow(), get_failed_symbol(), symbol_exprt::get_identifier(), ssa_exprt::get_object_name(), goto_symex_statet::guard, symex_targett::HIDDEN, goto_symex_statet::framet::hidden_function, goto_symex_statet::renaming_levelt::increase_counter(), irept::is_not_nil(), goto_symex_statet::L1, goto_symex_statet::level2, namespacet::lookup(), ns, address_of_exprt::object(), symex_targett::sourcet::pc, goto_symex_statet::propagation, goto_symex_statet::record_events, goto_symex_statet::propagationt::remove(), goto_symex_statet::rename(), symex_targett::shared_write(), goto_symex_statet::source, symex_targett::STATE, target, goto_symex_statet::top(), exprt::type(), ssa_exprt::update_type(), and goto_symex_statet::value_set.
|
protectedvirtual |
do function call by inlining
Definition at line 361 of file symex_function_call.cpp.
References guardt::as_expr(), symex_targett::function_return(), goto_symex_statet::guard, symex_targett::sourcet::pc, pop_frame(), goto_symex_statet::source, and target.
Referenced by symex_step().
|
protectedvirtual |
Definition at line 470 of file symex_builtin_functions.cpp.
References Forall_operands, and exprt::reserve_operands().
Referenced by symex_function_call_symbol().
|
protectedvirtual |
Definition at line 172 of file symex_function_call.cpp.
References code_function_callt::function(), and symex_function_call_symbol().
Referenced by symex_step().
|
protectedvirtual |
do function call by inlining
Definition at line 218 of file symex_function_call.cpp.
References guardt::add(), exprt::add_source_location(), code_function_callt::arguments(), guardt::as_expr(), goto_symex_statet::call_stack(), code_function_callt::function(), symex_targett::function_call(), goto_functions_templatet< bodyT >::function_map, symex_targett::function_return(), optionst::get_bool_option(), get_unwind_recursion(), goto_symex_statet::guard, id2string(), irept::is_not_nil(), symex_targett::sourcet::is_set, code_function_callt::lhs(), locality(), goto_symex_statet::framet::loop_iterations, goto_symex_statet::new_frame(), no_body(), ns, options, parameter_assignments(), goto_symex_statet::previous_frame(), goto_symex_statet::rename(), goto_symex_statet::source, exprt::source_location(), symex_assign_rec(), symex_transition(), target, symex_targett::sourcet::thread_nr, to_symbol_expr(), goto_symex_statet::top(), exprt::type(), and vcc().
Referenced by symex_function_call_symbol().
|
protectedvirtual |
Definition at line 189 of file symex_function_call.cpp.
References guardt::as_expr(), CPROVER_FKT_PREFIX, CPROVER_MACRO_PREFIX, code_function_callt::function(), goto_symex_statet::guard, has_prefix(), irept::id(), id2string(), symex_targett::location(), goto_symex_statet::source, symex_fkt(), symex_function_call_code(), symex_macro(), symex_trace(), target, and to_symbol_expr().
Referenced by symex_function_call().
|
protectedvirtual |
Definition at line 207 of file symex_builtin_functions.cpp.
References do_simplify(), get_symbol(), has_prefix(), id2string(), irept::is_nil(), namespacet::lookup(), exprt::make_typecast(), symbolt::name, ns, exprt::op0(), exprt::operands(), pos(), goto_symex_statet::rename(), safe_string2unsigned(), exprt::source_location(), symex_assign_rec(), symbolt::type, exprt::type(), and zero_initializer().
Referenced by symex_assign().
|
protectedvirtual |
Definition at line 21 of file symex_goto.cpp.
References guardt::add(), guardt::as_expr(), symex_targett::assignment(), goto_symex_statet::assignment(), clean_expr(), do_simplify(), get_unwind(), symex_targett::goto_instruction(), goto_symex_statet::framet::goto_state_map, goto_symex_statet::guard, symex_targett::GUARD, goto_symex_statet::goto_statet::guard, guard_identifier, irept::id(), exprt::is_false(), exprt::is_true(), goto_symex_statet::L1, symex_targett::location(), loop_bound_exceeded(), goto_program_templatet< codet, exprt >::loop_id(), goto_symex_statet::framet::loop_iterations, exprt::make_false(), exprt::make_not(), ns, exprt::op0(), exprt::operands(), symex_targett::sourcet::pc, goto_symex_statet::rename(), goto_symex_statet::source, symex_assume(), symex_transition(), target, and goto_symex_statet::top().
Referenced by symex_step().
Definition at line 314 of file symex_builtin_functions.cpp.
References guardt::as_expr(), do_simplify(), get_string_argument(), goto_symex_statet::guard, symex_targett::input(), ns, exprt::op0(), exprt::operands(), goto_symex_statet::rename(), goto_symex_statet::source, and target.
Referenced by symex_other().
|
protectedvirtual |
Definition at line 493 of file symex_builtin_functions.cpp.
References exprt::copy_to_operands(), CPROVER_MACRO_PREFIX, irept::get(), irept::id(), id2string(), exprt::op0(), exprt::op1(), exprt::op2(), exprt::op3(), and replace_expr().
Referenced by symex_function_call_symbol().
|
protectedvirtual |
Definition at line 54 of file symex_builtin_functions.cpp.
References symbol_tablet::add(), index_exprt::array(), symbolt::base_name, c_sizeof_type_rec(), dynamic_counter, 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, new_symbol_table, ns, exprt::op0(), exprt::op1(), exprt::operands(), pointer_offset_size(), pointer_type(), goto_symex_statet::rename(), irept::set(), simplify(), array_typet::size(), typet::subtype(), symbolt::symbol_expr(), symex_assign_rec(), to_array_type(), to_integer(), symbolt::type, exprt::type(), and unsigned_char_type().
Referenced by symex_assign().
|
protectedvirtual |
Definition at line 24 of file symex_other.cpp.
References guardt::as_expr(), base_type_eq(), byte_extract_id(), clean_expr(), namespace_baset::follow(), from_integer(), codet::get_statement(), goto_symex_statet::guard, id2string(), index_type(), code_assignt::lhs(), symex_targett::memory_barrier(), ns, byte_extract_exprt::offset(), byte_extract_exprt::op(), exprt::op0(), exprt::op1(), exprt::operands(), symex_targett::sourcet::pc, process_array_expr(), code_assignt::rhs(), goto_symex_statet::source, typet::subtype(), symex_assign(), symex_cpp_delete(), symex_input(), symex_output(), symex_printf(), target, to_array_type(), to_byte_extract_expr(), to_code(), and exprt::type().
Referenced by symex_step().
Definition at line 339 of file symex_builtin_functions.cpp.
References guardt::as_expr(), do_simplify(), get_string_argument(), goto_symex_statet::guard, ns, exprt::op0(), exprt::operands(), symex_targett::output(), goto_symex_statet::rename(), goto_symex_statet::source, and target.
Referenced by symex_other().
|
protectedvirtual |
Definition at line 287 of file symex_builtin_functions.cpp.
References guardt::as_expr(), do_simplify(), get_string_argument(), goto_symex_statet::guard, ns, exprt::operands(), symex_targett::output_fmt(), goto_symex_statet::rename(), goto_symex_statet::source, and target.
Referenced by symex_assign(), and symex_other().
|
protectedvirtual |
Definition at line 16 of file symex_start_thread.cpp.
References guardt::as_expr(), goto_symex_statet::atomic_section_id, goto_symex_statet::threadt::call_stack, goto_symex_statet::renaming_levelt::current_names, forall_symbols, namespacet::get_symbol_table(), goto_symex_statet::guard, goto_symex_statet::threadt::guard, symex_targett::HIDDEN, symbolt::is_extern, exprt::is_false(), irept::is_nil(), symbolt::is_static_lifetime, symbolt::is_thread_local, goto_symex_statet::L1, goto_symex_statet::l1_history, goto_symex_statet::level1, goto_symex_statet::level2, goto_symex_statet::framet::local_objects, symbolt::location, ns, symex_targett::sourcet::pc, goto_symex_statet::threadt::pc, goto_symex_statet::record_events, goto_symex_statet::rename(), ssa_exprt::set_level_0(), goto_symex_statet::source, symex_targett::spawn(), symbolt::symbol_expr(), symbol_tablet::symbols, symex_assign_symbol(), target, goto_symex_statet::threads, goto_symex_statet::top(), symbolt::type, symbolt::value, and zero_initializer().
Referenced by symex_step().
|
virtual |
execute just one step
do just one step
Reimplemented in symex_bmct.
Definition at line 188 of file symex_main.cpp.
References guardt::add(), code_function_callt::arguments(), guardt::as_expr(), ASSERT, ASSIGN, ASSUME, ATOMIC_BEGIN, ATOMIC_END, goto_symex_statet::call_stack(), CATCH, clean_expr(), DEAD, DECL, goto_symex_statet::depth, END_FUNCTION, END_THREAD, Forall_expr, from_expr(), code_function_callt::function(), FUNCTION_CALL, optionst::get_unsigned_int_option(), GOTO, goto_symex_statet::guard, id2string(), exprt::is_false(), irept::is_not_nil(), code_function_callt::lhs(), LOCATION, symex_targett::location(), merge_gotos(), NO_INSTRUCTION_TYPE, ns, options, OTHER, symex_targett::sourcet::pc, goto_symex_statet::rename(), RETURN, return_assignment(), SKIP, goto_symex_statet::source, START_THREAD, symex_assign_rec(), symex_assume(), symex_atomic_begin(), symex_atomic_end(), symex_catch(), symex_dead(), symex_decl(), symex_end_of_function(), symex_function_call(), symex_goto(), symex_other(), symex_start_thread(), symex_throw(), symex_transition(), target, goto_symex_statet::threads, THROW, to_code_assign(), to_code_function_call(), and vcc().
Referenced by operator()(), and symex_bmct::symex_step().
|
virtual |
Definition at line 193 of file symex_goto.cpp.
References guardt::as_expr(), symex_targett::assumption(), dereference(), do_simplify(), goto_symex_statet::guard, guardt::guard_expr(), exprt::make_not(), ns, symex_targett::sourcet::pc, goto_symex_statet::rename(), goto_symex_statet::source, and target.
|
protected |
Definition at line 14 of file symex_throw.cpp.
References goto_symex_statet::call_stack(), goto_symex_statet::framet::catch_map, symex_targett::sourcet::pc, goto_symex_statet::source, and symex_assume().
Referenced by symex_step().
|
protectedvirtual |
Definition at line 431 of file symex_builtin_functions.cpp.
References code_function_callt::arguments(), guardt::as_expr(), optionst::get_option(), goto_symex_statet::guard, ns, options, symex_targett::output(), goto_symex_statet::rename(), goto_symex_statet::source, target, to_integer(), and unsafe_string2int().
Referenced by symex_function_call_symbol().
|
protectedvirtual |
Definition at line 23 of file symex_main.cpp.
References goto_symex_statet::call_stack(), goto_program_templatet< codet, exprt >::loop_id(), goto_symex_statet::framet::loop_iterations, symex_targett::sourcet::pc, goto_symex_statet::source, and goto_symex_statet::top().
Referenced by operator()(), pop_frame(), symex_function_call_code(), symex_goto(), symex_step(), and symex_transition().
|
inlineprotectedvirtual |
Definition at line 159 of file goto_symex.h.
References symex_targett::sourcet::pc, goto_symex_statet::source, symex_dereference_statet::state, and symex_transition().
Definition at line 84 of file auto_objects.cpp.
References symbolt::base_name, goto_symex_statet::renaming_levelt::current_names, forall_operands, irept::get_bool(), symbol_exprt::get_identifier(), ssa_exprt::get_object_name(), has_prefix(), irept::id(), id2string(), initialize_auto_object(), goto_symex_statet::level2, namespacet::lookup(), ns, and to_ssa_expr().
Referenced by dereference_rec().
|
protectedvirtual |
Definition at line 53 of file symex_main.cpp.
References guardt::as_expr(), symex_targett::assertion(), do_simplify(), goto_symex_statet::guard, guardt::guard_expr(), exprt::is_true(), ns, remaining_vccs, goto_symex_statet::rename(), rewrite_quantifiers(), goto_symex_statet::source, target, and total_vccs.
Referenced by loop_bound_exceeded(), symex_function_call_code(), and symex_step().
|
friend |
Definition at line 108 of file goto_symex.h.
|
protected |
Definition at line 106 of file goto_symex.h.
Referenced by symex_atomic_begin().
bool goto_symext::constant_propagation |
Definition at line 94 of file goto_symex.h.
Referenced by bmct::bmct(), scratch_programt::check_sat(), and symex_assign_symbol().
|
staticprotected |
Definition at line 334 of file goto_symex.h.
Referenced by make_auto_object(), symex_cpp_new(), and symex_malloc().
|
protected |
Definition at line 152 of file goto_symex.h.
Referenced by phi_function(), and symex_goto().
irep_idt goto_symext::language_mode |
language_mode: ID_java, ID_C or another language identifier if we know the source language in use, irep_idt() otherwise.
Definition at line 101 of file goto_symex.h.
Referenced by dereference_rec(), and bmct::run().
symbol_tablet& goto_symext::new_symbol_table |
Definition at line 97 of file goto_symex.h.
Referenced by dereference_rec(), symex_dereference_statet::has_failed_symbol(), make_auto_object(), new_name(), parameter_assignments(), symex_cpp_new(), and symex_malloc().
|
staticprotected |
Definition at line 333 of file goto_symex.h.
Referenced by replace_nondet().
|
protected |
Definition at line 104 of file goto_symex.h.
Referenced by address_arithmetic(), dereference(), dereference_rec(), do_simplify(), symex_dereference_statet::get_value_set(), symex_dereference_statet::has_failed_symbol(), initialize_auto_object(), locality(), new_name(), parameter_assignments(), phi_function(), process_array_expr_rec(), replace_array_equal(), return_assignment(), symex_assign_array(), symex_assign_if(), symex_assign_rec(), symex_assign_struct_member(), symex_assign_symbol(), symex_dead(), symex_decl(), symex_function_call_code(), symex_gcc_builtin_va_arg_next(), symex_goto(), symex_input(), symex_malloc(), symex_other(), symex_output(), symex_printf(), symex_start_thread(), symex_step(), symex_bmct::symex_step(), symex_step_goto(), symex_trace(), trigger_auto_object(), and vcc().
optionst goto_symext::options |
Definition at line 96 of file goto_symex.h.
Referenced by dereference_rec(), do_simplify(), goto_symext(), loop_bound_exceeded(), bmct::run(), symex_assign_symbol(), symex_function_call_code(), symex_step(), and symex_trace().
unsigned goto_symext::remaining_vccs |
Definition at line 92 of file goto_symex.h.
Referenced by bmct::run(), and vcc().
|
protected |
Definition at line 105 of file goto_symex.h.
Referenced by operator()(), phi_function(), return_assignment(), symex_assign_symbol(), symex_assume(), symex_atomic_begin(), symex_atomic_end(), symex_decl(), symex_end_of_function(), symex_function_call_code(), symex_function_call_symbol(), symex_goto(), symex_input(), symex_other(), symex_output(), symex_printf(), symex_start_thread(), symex_step(), symex_step_goto(), symex_trace(), and vcc().
unsigned goto_symext::total_vccs |
Definition at line 92 of file goto_symex.h.
Referenced by bmct::run(), and vcc().