cprover
symex_bmc.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Bounded Model Checking for ANSI-C
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#ifndef CPROVER_GOTO_CHECKER_SYMEX_BMC_H
13#define CPROVER_GOTO_CHECKER_SYMEX_BMC_H
14
15#include <util/threeval.h>
16
18
19#include "symex_coverage.h"
20
21class unwindsett;
22
23class symex_bmct : public goto_symext
24{
25public:
30 const optionst &options,
34
35 // To show progress
37
44 typedef std::function<
45 tvt(const call_stackt &, unsigned, unsigned, unsigned &)>
47
54 typedef std::function<tvt(const irep_idt &, unsigned, unsigned &)>
56
62 {
63 loop_unwind_handlers.push_back(handler);
64 }
65
71 {
72 recursion_unwind_handlers.push_back(handler);
73 }
74
76 const goto_functionst &goto_functions,
77 const std::string &path) const
78 {
79 return symex_coverage.generate_report(goto_functions, path);
80 }
81
82 const bool record_coverage;
84
86
87protected:
89 std::vector<loop_unwind_handlert> loop_unwind_handlers;
90
93 std::vector<recursion_unwind_handlert> recursion_unwind_handlers;
94
96 override;
97
98 void merge_goto(
99 const symex_targett::sourcet &source,
100 goto_statet &&goto_state,
101 statet &state) override;
102
104 const symex_targett::sourcet &source,
105 const call_stackt &context,
106 unsigned unwind) override;
107
109 const irep_idt &identifier,
110 unsigned thread_nr,
111 unsigned unwind) override;
112
113 void no_body(const irep_idt &identifier) override;
114
115 std::unordered_set<irep_idt> body_warnings;
116
118};
119
120#endif // CPROVER_GOTO_CHECKER_SYMEX_BMC_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
A collection of goto functions.
Container for data that varies per program point, e.g.
Definition: goto_state.h:32
Central data structure: state.
The main class for the forward symbolic simulator.
Definition: goto_symex.h:35
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
path_storaget & path_storage
Symbolic execution paths to be resumed later.
Definition: goto_symex.h:788
guard_managert & guard_manager
Used to create guards.
Definition: goto_symex.h:248
const symbol_tablet & outer_symbol_table
The symbol table associated with the goto-program being executed.
Definition: goto_symex.h:234
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:82
Storage for symbolic execution paths to be resumed later.
Definition: path_storage.h:38
The symbol table.
Definition: symbol_table.h:14
const bool havoc_bodyless_functions
Definition: symex_bmc.h:83
symex_coveraget symex_coverage
Definition: symex_bmc.h:117
bool get_unwind_recursion(const irep_idt &identifier, unsigned thread_nr, unsigned unwind) override
Definition: symex_bmc.cpp:166
std::vector< loop_unwind_handlert > loop_unwind_handlers
Callbacks that may provide an unwind/do-not-unwind decision for a loop.
Definition: symex_bmc.h:89
unwindsett & unwindset
Definition: symex_bmc.h:85
void merge_goto(const symex_targett::sourcet &source, goto_statet &&goto_state, statet &state) override
Merge a single branch, the symbolic state of which is held in goto_state, into the current overall sy...
Definition: symex_bmc.cpp:100
std::function< tvt(const call_stackt &, unsigned, unsigned, unsigned &)> loop_unwind_handlert
Loop unwind handlers take the call stack, loop number, the unwind count so far, and an out-parameter ...
Definition: symex_bmc.h:46
source_locationt last_source_location
Definition: symex_bmc.h:36
bool output_coverage_report(const goto_functionst &goto_functions, const std::string &path) const
Definition: symex_bmc.h:75
void add_recursion_unwind_handler(recursion_unwind_handlert handler)
Add a callback function that will be called to determine whether to unwind recursion.
Definition: symex_bmc.h:70
std::unordered_set< irep_idt > body_warnings
Definition: symex_bmc.h:115
void no_body(const irep_idt &identifier) override
Log a warning that a function has no body.
Definition: symex_bmc.cpp:213
std::vector< recursion_unwind_handlert > recursion_unwind_handlers
Callbacks that may provide an unwind/do-not-unwind decision for a recursive call.
Definition: symex_bmc.h:93
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
void symex_step(const get_goto_functiont &get_goto_function, statet &state) override
show progress
Definition: symex_bmc.cpp:45
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.cpp:120
void add_loop_unwind_handler(loop_unwind_handlert handler)
Add a callback function that will be called to determine whether to unwind loops.
Definition: symex_bmc.h:61
const bool record_coverage
Definition: symex_bmc.h:82
std::function< tvt(const irep_idt &, unsigned, unsigned &)> recursion_unwind_handlert
Recursion unwind handlers take the function ID, the unwind count so far, and an out-parameter specify...
Definition: symex_bmc.h:55
bool generate_report(const goto_functionst &goto_functions, const std::string &path) const
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
Definition: threeval.h:20
Symbolic Execution.
This is unused by this implementation of guards, but can be used by other implementations of the same...
Definition: guard_expr.h:20
Identifies source in the context of symbolic execution.
Definition: symex_target.h:37
Record and print code coverage of symbolic execution.