|
| symex_bmct (message_handlert &mh, const symbol_tablet &outer_symbol_table, symex_target_equationt &_target, const optionst &options, path_storaget &path_storage) |
|
void | add_loop_unwind_handler (loop_unwind_handlert handler) |
| Add a callback function that will be called to determine whether to unwind loops. More...
|
|
void | add_recursion_unwind_handler (recursion_unwind_handlert handler) |
| Add a callback function that will be called to determine whether to unwind recursion. More...
|
|
bool | output_coverage_report (const goto_functionst &goto_functions, const std::string &path) const |
|
| goto_symext (message_handlert &mh, const symbol_tablet &outer_symbol_table, symex_target_equationt &_target, const optionst &options, path_storaget &path_storage) |
|
virtual | ~goto_symext ()=default |
|
virtual void | symex_from_entry_point_of (const get_goto_functiont &get_goto_function, symbol_tablet &new_symbol_table) |
| symex entire program starting from entry point More...
|
|
virtual void | resume_symex_from_saved_state (const get_goto_functiont &get_goto_function, const statet &saved_state, symex_target_equationt *saved_equation, symbol_tablet &new_symbol_table) |
| Performs symbolic execution using a state and equation that have already been used to symex part of the program. More...
|
|
virtual void | symex_with_state (statet &, const goto_functionst &, symbol_tablet &) |
| symex entire program starting from entry point More...
|
|
virtual void | symex_with_state (statet &, const get_goto_functiont &, symbol_tablet &) |
| symex entire program starting from entry point More...
|
|
unsigned | get_total_vccs () |
|
unsigned | get_remaining_vccs () |
|
void | validate (const namespacet &ns, const validation_modet vm) const |
|
|
void | symex_step (const get_goto_functiont &get_goto_function, statet &state) override |
| show progress More...
|
|
void | merge_goto (const statet::goto_statet &goto_state, statet &state) override |
|
bool | should_stop_unwind (const symex_targett::sourcet &source, const goto_symex_statet::call_stackt &context, unsigned unwind) override |
|
bool | get_unwind_recursion (const irep_idt &identifier, const unsigned thread_nr, unsigned unwind) override |
|
void | no_body (const irep_idt &identifier) override |
|
void | initialize_entry_point (statet &state, const get_goto_functiont &get_goto_function, const irep_idt &function_identifier, goto_programt::const_targett pc, goto_programt::const_targett limit) |
| Initialise the symbolic execution and the given state with pc as entry point. More...
|
|
void | symex_threaded_step (statet &, const get_goto_functiont &) |
| Invokes symex_step and verifies whether additional threads can be executed. More...
|
|
void | clean_expr (exprt &, statet &, bool write) |
|
void | trigger_auto_object (const exprt &, statet &) |
|
void | initialize_auto_object (const exprt &, statet &) |
|
void | process_array_expr (exprt &) |
| Given an expression, find the root object and the offset into it. More...
|
|
exprt | make_auto_object (const typet &, statet &) |
|
virtual void | dereference (exprt &, statet &, bool write) |
|
void | dereference_rec (exprt &, statet &, guardt &, bool write) |
|
void | dereference_rec_address_of (exprt &, statet &, guardt &) |
|
exprt | address_arithmetic (const exprt &, statet &, guardt &, bool keep_array) |
| Evaluate an ID_address_of expression. More...
|
|
virtual void | symex_goto (statet &) |
|
virtual void | symex_start_thread (statet &) |
|
virtual void | symex_atomic_begin (statet &) |
|
virtual void | symex_atomic_end (statet &) |
|
virtual void | symex_decl (statet &) |
|
virtual void | symex_decl (statet &, const symbol_exprt &expr) |
|
virtual void | symex_dead (statet &) |
|
virtual void | symex_other (statet &) |
|
virtual void | vcc (const exprt &, const std::string &msg, statet &) |
|
virtual void | symex_assume (statet &, const exprt &cond) |
|
void | merge_gotos (statet &) |
|
void | merge_value_sets (const statet::goto_statet &goto_state, statet &dest) |
|
void | phi_function (const statet::goto_statet &goto_state, statet &) |
|
virtual void | loop_bound_exceeded (statet &, const exprt &guard) |
|
void | pop_frame (statet &) |
| pop one call frame More...
|
|
void | return_assignment (statet &) |
|
virtual void | symex_function_call (const get_goto_functiont &, statet &, const code_function_callt &) |
|
virtual void | symex_end_of_function (statet &) |
| do function call by inlining More...
|
|
virtual void | symex_function_call_symbol (const get_goto_functiont &, statet &, const code_function_callt &) |
|
virtual void | symex_function_call_code (const get_goto_functiont &, statet &, const code_function_callt &) |
| do function call by inlining More...
|
|
void | parameter_assignments (const irep_idt &function_identifier, const goto_functionst::goto_functiont &, statet &, const exprt::operandst &arguments) |
|
void | locality (const irep_idt &function_identifier, statet &, const goto_functionst::goto_functiont &) |
| preserves locality of local variables of a given function by applying L1 renaming to the local identifiers More...
|
|
void | symex_throw (statet &) |
|
void | symex_catch (statet &) |
|
virtual void | do_simplify (exprt &) |
|
void | symex_assign (statet &, const code_assignt &) |
|
void | havoc_rec (statet &, const guardt &, const exprt &) |
|
void | symex_assign_rec (statet &, const exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &, assignment_typet) |
|
void | symex_assign_symbol (statet &, const ssa_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &, assignment_typet) |
|
void | symex_assign_typecast (statet &, const typecast_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &, assignment_typet) |
|
void | symex_assign_array (statet &, const index_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &, assignment_typet) |
|
void | symex_assign_struct_member (statet &, const member_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &, assignment_typet) |
|
void | symex_assign_if (statet &, const if_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &, assignment_typet) |
|
void | symex_assign_byte_extract (statet &, const byte_extract_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &, assignment_typet) |
|
virtual void | symex_gcc_builtin_va_arg_next (statet &, const exprt &lhs, const side_effect_exprt &) |
|
virtual void | symex_allocate (statet &, const exprt &lhs, const side_effect_exprt &) |
|
virtual void | symex_cpp_delete (statet &, const codet &) |
|
virtual void | symex_cpp_new (statet &, const exprt &lhs, const side_effect_exprt &) |
| Handles side effects of type 'new' for C++ and 'new array' for C++ and Java language modes. More...
|
|
virtual void | symex_fkt (statet &, const code_function_callt &) |
|
virtual void | symex_macro (statet &, const code_function_callt &) |
|
virtual void | symex_trace (statet &, const code_function_callt &) |
|
virtual void | symex_printf (statet &, const exprt &rhs) |
|
virtual void | symex_input (statet &, const codet &) |
|
virtual void | symex_output (statet &, const codet &) |
|
void | rewrite_quantifiers (exprt &, statet &) |
|
Definition at line 25 of file symex_bmc.h.