cprover
symex_bmc_incremental_one_loop.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3  Module: Incremental Bounded Model Checking for ANSI-C
4 
5  Author: Peter Schrammel, Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #ifndef CPROVER_GOTO_CHECKER_SYMEX_BMC_INCREMENTAL_ONE_LOOP_H
10 #define CPROVER_GOTO_CHECKER_SYMEX_BMC_INCREMENTAL_ONE_LOOP_H
11 
12 #include "symex_bmc.h"
13 #include <util/ui_message.h>
14 
16 {
17 public:
22  const optionst &,
23  path_storaget &,
26 
30  symbol_tablet &new_symbol_table);
31 
34 
35 protected:
37  const unsigned incr_max_unwind;
38  const unsigned incr_min_unwind;
39 
40  std::unique_ptr<goto_symext::statet> state;
41 
42  // returns true if the symbolic execution is to be interrupted for checking
43  bool check_break(const irep_idt &loop_id, unsigned unwind) override;
44 
45  bool should_stop_unwind(
46  const symex_targett::sourcet &source,
47  const call_stackt &context,
48  unsigned unwind) override;
49 
50  void log_unwinding(unsigned unwind);
51 
53 };
54 
55 #endif // CPROVER_GOTO_CHECKER_SYMEX_BMC_INCREMENTAL_ONE_LOOP_H
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
symex_bmc_incremental_one_loopt
Definition: symex_bmc_incremental_one_loop.h:16
optionst
Definition: options.h:23
path_storaget
Storage for symbolic execution paths to be resumed later.
Definition: path_storage.h:38
symex_bmc_incremental_one_loopt::check_break
bool check_break(const irep_idt &loop_id, unsigned unwind) override
Defines condition for interrupting symbolic execution for incremental BMC.
Definition: symex_bmc_incremental_one_loop.cpp:111
call_stackt
Definition: call_stack.h:15
ui_message_handlert::uit
uit
Definition: ui_message.h:22
symex_bmc_incremental_one_loopt::output_ui
ui_message_handlert::uit output_ui
Definition: symex_bmc_incremental_one_loop.h:52
guard_expr_managert
This is unused by this implementation of guards, but can be used by other implementations of the same...
Definition: guard_expr.h:23
goto_symext::outer_symbol_table
const symbol_tablet & outer_symbol_table
The symbol table associated with the goto-program being executed.
Definition: goto_symex.h:247
symex_bmc_incremental_one_loopt::state
std::unique_ptr< goto_symext::statet > state
Definition: symex_bmc_incremental_one_loop.h:40
message_handlert
Definition: message.h:28
symex_bmc_incremental_one_loopt::incr_max_unwind
const unsigned incr_max_unwind
Definition: symex_bmc_incremental_one_loop.h:37
symex_target_equationt
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
Definition: symex_target_equation.h:41
symex_bmc_incremental_one_loopt::should_stop_unwind
bool should_stop_unwind(const symex_targett::sourcet &source, const call_stackt &context, unsigned unwind) override
Determine whether to unwind a loop.
Definition: symex_bmc_incremental_one_loop.cpp:49
goto_symext::get_goto_function
static get_goto_functiont get_goto_function(abstract_goto_modelt &goto_model)
Return a function to get/load a goto function from the given goto model Create a default delegate to ...
Definition: symex_main.cpp:493
symex_bmc_incremental_one_loopt::incr_min_unwind
const unsigned incr_min_unwind
Definition: symex_bmc_incremental_one_loop.h:38
symex_bmc_incremental_one_loopt::incr_loop_id
const irep_idt incr_loop_id
Definition: symex_bmc_incremental_one_loop.h:36
symex_bmc_incremental_one_loopt::resume
bool resume(const get_goto_functiont &get_goto_function)
Return true if symex can be resumed.
Definition: symex_bmc_incremental_one_loop.cpp:133
goto_symext::get_goto_functiont
std::function< const goto_functionst::goto_functiont &(const irep_idt &)> get_goto_functiont
The type of delegate functions that retrieve a goto_functiont for a particular function identifier.
Definition: goto_symex.h:95
symex_bmc_incremental_one_loopt::symex_bmc_incremental_one_loopt
symex_bmc_incremental_one_loopt(message_handlert &, const symbol_tablet &outer_symbol_table, symex_target_equationt &, const optionst &, path_storaget &, guard_managert &, ui_message_handlert::uit output_ui)
Definition: symex_bmc_incremental_one_loop.cpp:16
symex_bmct
Definition: symex_bmc.h:26
symex_bmc_incremental_one_loopt::log_unwinding
void log_unwinding(unsigned unwind)
Definition: symex_bmc_incremental_one_loop.cpp:142
symex_targett::sourcet
Identifies source in the context of symbolic execution.
Definition: symex_target.h:38
symex_bmc_incremental_one_loopt::from_entry_point_of
bool from_entry_point_of(const get_goto_functiont &get_goto_function, symbol_tablet &new_symbol_table)
Return true if symex can be resumed.
Definition: symex_bmc_incremental_one_loop.cpp:122
symex_bmc.h
Bounded Model Checking for ANSI-C.
ui_message.h