cprover
Loading...
Searching...
No Matches
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{
17public:
22 const optionst &,
25 unwindsett &,
27
31 symbol_tablet &new_symbol_table);
32
35
36protected:
38 const unsigned incr_max_unwind;
39 const unsigned incr_min_unwind;
40
41 std::unique_ptr<goto_symext::statet> state;
42
43 // returns true if the symbolic execution is to be interrupted for checking
44 bool check_break(const irep_idt &loop_id, unsigned unwind) override;
45
47 const symex_targett::sourcet &source,
48 const call_stackt &context,
49 unsigned unwind) override;
50
51 void log_unwinding(unsigned unwind);
52
54};
55
56#endif // CPROVER_GOTO_CHECKER_SYMEX_BMC_INCREMENTAL_ONE_LOOP_H
const symbol_table_baset & outer_symbol_table
The symbol table associated with the goto-program being executed.
Definition goto_symex.h:250
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 ...
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:94
Storage for symbolic execution paths to be resumed later.
The symbol table.
bool resume(const get_goto_functiont &get_goto_function)
Return true if symex can be resumed.
symex_bmc_incremental_one_loopt(message_handlert &, const symbol_tablet &outer_symbol_table, symex_target_equationt &, const optionst &, path_storaget &, guard_managert &, unwindsett &, ui_message_handlert::uit output_ui)
bool from_entry_point_of(const get_goto_functiont &get_goto_function, symbol_tablet &new_symbol_table)
Return true if symex can be resumed.
bool check_break(const irep_idt &loop_id, unsigned unwind) override
Defines condition for interrupting symbolic execution for incremental BMC.
std::unique_ptr< goto_symext::statet > state
bool should_stop_unwind(const symex_targett::sourcet &source, const call_stackt &context, unsigned unwind) override
Determine whether to unwind a loop.
symex_bmct(message_handlert &mh, const symbol_tablet &outer_symbol_table, symex_target_equationt &_target, const optionst &options, path_storaget &path_storage, guard_managert &guard_manager, unwindsett &unwindset)
Definition symex_bmc.cpp:21
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
guard_expr_managert guard_managert
Definition guard.h:28
Identifies source in the context of symbolic execution.
Bounded Model Checking for ANSI-C.
dstringt irep_idt