cprover
|
#include <symex_bmc.h>
Public Member Functions | |
symex_bmct (const namespacet &_ns, symbol_tablet &_new_symbol_table, symex_targett &_target) | |
void | set_unwind_limit (unsigned limit) |
void | set_unwind_thread_loop_limit (unsigned thread_nr, const irep_idt &id, unsigned limit) |
void | set_unwind_loop_limit (const irep_idt &id, unsigned limit) |
bool | output_coverage_report (const goto_functionst &goto_functions, const std::string &path) const |
![]() | |
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_goto (statet &state, bool taken) |
Public Attributes | |
source_locationt | last_source_location |
bool | record_coverage |
![]() | |
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 std::unordered_map< irep_idt, unsigned, irep_id_hash > | loop_limitst |
typedef std::map< unsigned, loop_limitst > | thread_loop_limitst |
![]() | |
typedef symex_targett::assignment_typet | assignment_typet |
Protected Member Functions | |
virtual void | symex_step (const goto_functionst &goto_functions, statet &state) |
show progress More... | |
virtual void | merge_goto (const statet::goto_statet &goto_state, statet &state) |
virtual bool | get_unwind (const symex_targett::sourcet &source, unsigned unwind) |
virtual bool | get_unwind_recursion (const irep_idt &identifier, const unsigned thread_nr, unsigned unwind) |
virtual void | no_body (const irep_idt &identifier) |
![]() | |
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) |
void | merge_value_sets (const statet::goto_statet &goto_state, statet &dest) |
void | phi_function (const statet::goto_statet &goto_state, statet &state) |
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 | 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... | |
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) |
Protected Attributes | |
unsigned | max_unwind |
bool | max_unwind_is_set |
loop_limitst | loop_limits |
thread_loop_limitst | thread_loop_limits |
std::unordered_set< irep_idt, irep_id_hash > | body_warnings |
symex_coveraget | symex_coverage |
![]() | |
const namespacet & | ns |
symex_targett & | target |
unsigned | atomic_section_counter |
irep_idt | guard_identifier |
Additional Inherited Members | |
![]() | |
typedef goto_symex_statet | statet |
![]() | |
static bool | is_index_member_symbol_if (const exprt &expr) |
static exprt | add_to_lhs (const exprt &lhs, const exprt &what) |
![]() | |
static unsigned | nondet_count =0 |
static unsigned | dynamic_counter =0 |
Definition at line 21 of file symex_bmc.h.
|
protected |
Definition at line 76 of file symex_bmc.h.
|
protected |
Definition at line 79 of file symex_bmc.h.
symex_bmct::symex_bmct | ( | const namespacet & | _ns, |
symbol_tablet & | _new_symbol_table, | ||
symex_targett & | _target | ||
) |
Definition at line 19 of file symex_bmc.cpp.
|
protectedvirtual |
Reimplemented from goto_symext.
Definition at line 106 of file symex_bmc.cpp.
References messaget::eom(), goto_program_templatet< codet, exprt >::loop_id(), loop_limits, max_unwind, max_unwind_is_set, symex_targett::sourcet::pc, messaget::mstreamt::source_location, messaget::statistics(), thread_loop_limits, and symex_targett::sourcet::thread_nr.
|
protectedvirtual |
Reimplemented from goto_symext.
Definition at line 147 of file symex_bmc.cpp.
References symbolt::display_name(), messaget::eom(), namespacet::lookup(), loop_limits, max_unwind, max_unwind_is_set, goto_symext::ns, messaget::statistics(), and thread_loop_limits.
|
protectedvirtual |
Reimplemented from goto_symext.
Definition at line 87 of file symex_bmc.cpp.
References symex_coveraget::covered(), goto_symex_statet::guard, goto_symex_statet::goto_statet::guard, exprt::is_false(), goto_symext::merge_goto(), symex_targett::sourcet::pc, record_coverage, goto_symex_statet::source, goto_symex_statet::goto_statet::source, and symex_coverage.
|
protectedvirtual |
Reimplemented from goto_symext.
Definition at line 192 of file symex_bmc.cpp.
References body_warnings, messaget::eom(), and messaget::warning().
|
inline |
Definition at line 57 of file symex_bmc.h.
References symex_coveraget::generate_report(), and symex_coverage.
Referenced by bmct::run().
|
inline |
Definition at line 36 of file symex_bmc.h.
References max_unwind, and max_unwind_is_set.
Referenced by bmct::setup_unwind().
|
inline |
Definition at line 50 of file symex_bmc.h.
References loop_limits.
Referenced by bmct::setup_unwind().
|
inline |
Definition at line 42 of file symex_bmc.h.
References thread_loop_limits.
Referenced by bmct::setup_unwind().
|
protectedvirtual |
show progress
Reimplemented from goto_symext.
Definition at line 31 of file symex_bmc.cpp.
References symex_coveraget::covered(), messaget::debug(), dstringt::empty(), goto_functions_templatet< bodyT >::entry_point(), messaget::eom(), source_locationt::get_file(), source_locationt::get_function(), source_locationt::get_line(), goto_symex_statet::guard, exprt::is_false(), irept::is_nil(), last_source_location, goto_symext::ns, symex_targett::sourcet::pc, record_coverage, simplify_expr(), goto_symex_statet::source, messaget::statistics(), symex_coverage, goto_symext::symex_step(), and symex_targett::sourcet::thread_nr.
|
protected |
Definition at line 105 of file symex_bmc.h.
Referenced by no_body().
source_locationt symex_bmct::last_source_location |
Definition at line 32 of file symex_bmc.h.
Referenced by bmct::run(), and symex_step().
|
protected |
Definition at line 77 of file symex_bmc.h.
Referenced by get_unwind(), get_unwind_recursion(), and set_unwind_loop_limit().
|
protected |
Definition at line 73 of file symex_bmc.h.
Referenced by get_unwind(), get_unwind_recursion(), and set_unwind_limit().
|
protected |
Definition at line 74 of file symex_bmc.h.
Referenced by get_unwind(), get_unwind_recursion(), and set_unwind_limit().
bool symex_bmct::record_coverage |
Definition at line 64 of file symex_bmc.h.
Referenced by bmct::bmct(), merge_goto(), and symex_step().
|
protected |
Definition at line 107 of file symex_bmc.h.
Referenced by merge_goto(), output_coverage_report(), and symex_step().
|
protected |
Definition at line 80 of file symex_bmc.h.
Referenced by get_unwind(), get_unwind_recursion(), and set_unwind_thread_loop_limit().