CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
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
15#include <util/irep.h>
16
17#include <list>
18#include <map>
19#include <optional>
20#include <string>
21
24
26{
27public:
28 // We have
29 // 1) a global limit
30 // 2) a limit per loop, all threads
31 // 3) a limit for a particular thread.
32 // We use the most specific of the above.
36
37 // global limit for all loops
38 void parse_unwind(const std::string &unwind);
39
40 // limit for instances of a loop
41 void parse_unwindset(
42 const std::list<std::string> &unwindset,
43 message_handlert &message_handler);
44
45 // queries
46 std::optional<unsigned>
47 get_limit(const irep_idt &loop, unsigned thread_id) const;
48
49 // read unwindset directives from a file
51 const std::string &file_name,
52 message_handlert &message_handler);
53
54protected:
56
57 std::optional<unsigned> global_limit;
58
59 // Limit for all instances of a loop.
60 // This may have 'no value'.
61 typedef std::map<irep_idt, std::optional<unsigned>> loop_mapt;
63
64 // separate limits per thread
66 std::map<std::pair<irep_idt, unsigned>, std::optional<unsigned>>;
68
70 std::string loop_limit,
71 message_handlert &message_handler);
72};
73
74#define OPT_UNWINDSET \
75 "(show-loops)" \
76 "(unwind):" \
77 "(unwindset):"
78
79#define HELP_UNWINDSET \
80 " {y--show-loops} \t show the loops in the program\n" \
81 " {y--unwind} {unr} \t unwind loops {unr} times\n" \
82 " {y--unwindset} [{uT}{y:}]{uL}{y:}{uB},... \t " \
83 "unwind loop {uL} with a bound of {uB} (optionally restricted to thread " \
84 "{uT}) (use {y--show-loops} to get the loop IDs)\n"
85
86#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:38
loop_mapt loop_map
Definition unwindset.h:62
std::optional< unsigned > get_limit(const irep_idt &loop, unsigned thread_id) const
void parse_unwindset_one_loop(std::string loop_limit, message_handlert &message_handler)
Definition unwindset.cpp:29
void parse_unwind(const std::string &unwind)
Definition unwindset.cpp:23
std::map< std::pair< irep_idt, unsigned >, std::optional< unsigned > > thread_loop_mapt
Definition unwindset.h:66
std::optional< unsigned > global_limit
Definition unwindset.h:57
thread_loop_mapt thread_loop_map
Definition unwindset.h:67
unwindsett(abstract_goto_modelt &goto_model)
Definition unwindset.h:33
void parse_unwindset_file(const std::string &file_name, message_handlert &message_handler)
abstract_goto_modelt & goto_model
Definition unwindset.h:55
std::map< irep_idt, std::optional< unsigned > > loop_mapt
Definition unwindset.h:61
void parse_unwindset(const std::list< std::string > &unwindset, message_handlert &message_handler)
const std::string thread_id