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 
15 {
16 public:
21  const optionst &,
22  path_storaget &,
23  guard_managert &);
24 
28  symbol_tablet &new_symbol_table);
29 
32 
33 protected:
35  const unsigned incr_max_unwind;
36  const unsigned incr_min_unwind;
37 
38  std::unique_ptr<goto_symext::statet> state;
39 
40  // returns true if the symbolic execution is to be interrupted for checking
41  bool check_break(const irep_idt &loop_id, unsigned unwind) override;
42 
43  bool should_stop_unwind(
44  const symex_targett::sourcet &source,
45  const call_stackt &context,
46  unsigned unwind) override;
47 };
48 
49 #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:15
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:103
call_stackt
Definition: call_stack.h:15
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:38
message_handlert
Definition: message.h:27
symex_bmc_incremental_one_loopt::incr_max_unwind
const unsigned incr_max_unwind
Definition: symex_bmc_incremental_one_loop.h:35
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:39
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:43
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:491
symex_bmc_incremental_one_loopt::incr_min_unwind
const unsigned incr_min_unwind
Definition: symex_bmc_incremental_one_loop.h:36
symex_bmc_incremental_one_loopt::incr_loop_id
const irep_idt incr_loop_id
Definition: symex_bmc_incremental_one_loop.h:34
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:125
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_bmct
Definition: symex_bmc.h:26
symex_targett::sourcet
Identifies source in the context of symbolic execution.
Definition: symex_target.h:38
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 &)
Definition: symex_bmc_incremental_one_loop.cpp:16
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:114
symex_bmc.h