cprover
unwindset.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Loop unwinding setup
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#ifndef CPROVER_GOTO_INSTRUMENT_UNWINDSET_H
13#define CPROVER_GOTO_INSTRUMENT_UNWINDSET_H
14
16
17#include <list>
18#include <map>
19#include <string>
20
22
24{
25public:
26 // We have
27 // 1) a global limit
28 // 2) a limit per loop, all threads
29 // 3) a limit for a particular thread.
30 // We use the most specific of the above.
32 {
33 }
34
35 // global limit for all loops
36 void parse_unwind(const std::string &unwind);
37
38 // limit for instances of a loop
39 void parse_unwindset(
40 const std::list<std::string> &unwindset,
41 message_handlert &message_handler);
42
43 // queries
44 optionalt<unsigned> get_limit(const irep_idt &loop, unsigned thread_id) const;
45
46 // read unwindset directives from a file
48 const std::string &file_name,
49 message_handlert &message_handler);
50
51protected:
53
55
56 // Limit for all instances of a loop.
57 // This may have 'no value'.
58 typedef std::map<irep_idt, optionalt<unsigned>> loop_mapt;
60
61 // separate limits per thread
63 std::map<std::pair<irep_idt, unsigned>, optionalt<unsigned>>;
65
67 std::string loop_limit,
68 message_handlert &message_handler);
69};
70
71#define OPT_UNWINDSET \
72 "(show-loops)" \
73 "(unwind):" \
74 "(unwindset):"
75
76#define HELP_UNWINDSET \
77 " --show-loops show the loops in the program\n" \
78 " --unwind nr unwind nr times\n" \
79 " --unwindset [T:]L:B,... unwind loop L with a bound of B\n" \
80 " (optionally restricted to thread T)\n" \
81 " (use --show-loops to get the loop IDs)\n"
82
83#endif // CPROVER_GOTO_INSTRUMENT_UNWINDSET_H
Abstract interface to eager or lazy GOTO models.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
loop_mapt loop_map
Definition: unwindset.h:59
void parse_unwindset_one_loop(std::string loop_limit, message_handlert &message_handler)
Definition: unwindset.cpp:28
void parse_unwind(const std::string &unwind)
Definition: unwindset.cpp:22
std::map< irep_idt, optionalt< unsigned > > loop_mapt
Definition: unwindset.h:58
optionalt< unsigned > global_limit
Definition: unwindset.h:54
std::map< std::pair< irep_idt, unsigned >, optionalt< unsigned > > thread_loop_mapt
Definition: unwindset.h:63
thread_loop_mapt thread_loop_map
Definition: unwindset.h:64
unwindsett(abstract_goto_modelt &goto_model)
Definition: unwindset.h:31
void parse_unwindset_file(const std::string &file_name, message_handlert &message_handler)
Definition: unwindset.cpp:204
abstract_goto_modelt & goto_model
Definition: unwindset.h:52
optionalt< unsigned > get_limit(const irep_idt &loop, unsigned thread_id) const
Definition: unwindset.cpp:183
void parse_unwindset(const std::list< std::string > &unwindset, message_handlert &message_handler)
Definition: unwindset.cpp:168
Symbol Table + CFG.
const std::string thread_id
nonstd::optional< T > optionalt
Definition: optional.h:35