cprover
symex_bmct Class Reference

#include <symex_bmc.h>

Inheritance diagram for symex_bmct:
[legend]
Collaboration diagram for symex_bmct:
[legend]

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
 
- Public Member Functions inherited from goto_symext
 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 Member Functions inherited from messaget
virtual void set_message_handler (message_handlert &_message_handler)
 
message_handlertget_message_handler ()
 
 messaget ()
 
 messaget (const messaget &other)
 
 messaget (message_handlert &_message_handler)
 
virtual ~messaget ()
 
mstreamtget_mstream (unsigned message_level)
 
mstreamterror ()
 
mstreamtwarning ()
 
mstreamtresult ()
 
mstreamtstatus ()
 
mstreamtstatistics ()
 
mstreamtprogress ()
 
mstreamtdebug ()
 

Public Attributes

source_locationt last_source_location
 
bool record_coverage
 
- Public Attributes inherited from goto_symext
unsigned total_vccs
 
unsigned remaining_vccs
 
bool constant_propagation
 
optionst options
 
symbol_tabletnew_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_hashloop_limitst
 
typedef std::map< unsigned, loop_limitstthread_loop_limitst
 
- Protected Types inherited from goto_symext
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)
 
- Protected Member Functions inherited from goto_symext
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_hashbody_warnings
 
symex_coveraget symex_coverage
 
- Protected Attributes inherited from goto_symext
const namespacetns
 
symex_targetttarget
 
unsigned atomic_section_counter
 
irep_idt guard_identifier
 
- Protected Attributes inherited from messaget
message_handlertmessage_handler
 
mstreamt mstream
 

Additional Inherited Members

- Public Types inherited from goto_symext
typedef goto_symex_statet statet
 
- Public Types inherited from messaget
enum  message_levelt {
  M_ERROR =1, M_WARNING =2, M_RESULT =4, M_STATUS =6,
  M_STATISTICS =8, M_PROGRESS =9, M_DEBUG =10
}
 
- Static Public Member Functions inherited from messaget
static mstreamteom (mstreamt &m)
 
static mstreamtendl (mstreamt &m)
 
- Static Protected Member Functions inherited from goto_symext
static bool is_index_member_symbol_if (const exprt &expr)
 
static exprt add_to_lhs (const exprt &lhs, const exprt &what)
 
- Static Protected Attributes inherited from goto_symext
static unsigned nondet_count =0
 
static unsigned dynamic_counter =0
 

Detailed Description

Definition at line 21 of file symex_bmc.h.

Member Typedef Documentation

§ loop_limitst

typedef std::unordered_map<irep_idt, unsigned, irep_id_hash> symex_bmct::loop_limitst
protected

Definition at line 76 of file symex_bmc.h.

§ thread_loop_limitst

typedef std::map<unsigned, loop_limitst> symex_bmct::thread_loop_limitst
protected

Definition at line 79 of file symex_bmc.h.

Constructor & Destructor Documentation

§ symex_bmct()

symex_bmct::symex_bmct ( const namespacet _ns,
symbol_tablet _new_symbol_table,
symex_targett _target 
)

Definition at line 19 of file symex_bmc.cpp.

Member Function Documentation

§ get_unwind()

§ get_unwind_recursion()

bool symex_bmct::get_unwind_recursion ( const irep_idt identifier,
const unsigned  thread_nr,
unsigned  unwind 
)
protectedvirtual

§ merge_goto()

§ no_body()

void symex_bmct::no_body ( const irep_idt identifier)
protectedvirtual

Reimplemented from goto_symext.

Definition at line 192 of file symex_bmc.cpp.

References body_warnings, messaget::eom(), and messaget::warning().

§ output_coverage_report()

bool symex_bmct::output_coverage_report ( const goto_functionst goto_functions,
const std::string &  path 
) const
inline

Definition at line 57 of file symex_bmc.h.

References symex_coveraget::generate_report(), and symex_coverage.

Referenced by bmct::run().

§ set_unwind_limit()

void symex_bmct::set_unwind_limit ( unsigned  limit)
inline

Definition at line 36 of file symex_bmc.h.

References max_unwind, and max_unwind_is_set.

Referenced by bmct::setup_unwind().

§ set_unwind_loop_limit()

void symex_bmct::set_unwind_loop_limit ( const irep_idt id,
unsigned  limit 
)
inline

Definition at line 50 of file symex_bmc.h.

References loop_limits.

Referenced by bmct::setup_unwind().

§ set_unwind_thread_loop_limit()

void symex_bmct::set_unwind_thread_loop_limit ( unsigned  thread_nr,
const irep_idt id,
unsigned  limit 
)
inline

Definition at line 42 of file symex_bmc.h.

References thread_loop_limits.

Referenced by bmct::setup_unwind().

§ symex_step()

Member Data Documentation

§ body_warnings

std::unordered_set<irep_idt, irep_id_hash> symex_bmct::body_warnings
protected

Definition at line 105 of file symex_bmc.h.

Referenced by no_body().

§ last_source_location

source_locationt symex_bmct::last_source_location

Definition at line 32 of file symex_bmc.h.

Referenced by bmct::run(), and symex_step().

§ loop_limits

loop_limitst symex_bmct::loop_limits
protected

Definition at line 77 of file symex_bmc.h.

Referenced by get_unwind(), get_unwind_recursion(), and set_unwind_loop_limit().

§ max_unwind

unsigned symex_bmct::max_unwind
protected

Definition at line 73 of file symex_bmc.h.

Referenced by get_unwind(), get_unwind_recursion(), and set_unwind_limit().

§ max_unwind_is_set

bool symex_bmct::max_unwind_is_set
protected

Definition at line 74 of file symex_bmc.h.

Referenced by get_unwind(), get_unwind_recursion(), and set_unwind_limit().

§ record_coverage

bool symex_bmct::record_coverage

Definition at line 64 of file symex_bmc.h.

Referenced by bmct::bmct(), merge_goto(), and symex_step().

§ symex_coverage

symex_coveraget symex_bmct::symex_coverage
protected

Definition at line 107 of file symex_bmc.h.

Referenced by merge_goto(), output_coverage_report(), and symex_step().

§ thread_loop_limits

thread_loop_limitst symex_bmct::thread_loop_limits
protected

Definition at line 80 of file symex_bmc.h.

Referenced by get_unwind(), get_unwind_recursion(), and set_unwind_thread_loop_limit().


The documentation for this class was generated from the following files: