12 #ifndef CPROVER_GOTO_INSTRUMENT_UNWINDSET_H
13 #define CPROVER_GOTO_INSTRUMENT_UNWINDSET_H
42 const std::list<std::string> &unwindset,
46 std::optional<unsigned>
51 const std::string &file_name,
61 typedef std::map<irep_idt, std::optional<unsigned>>
loop_mapt;
66 std::map<std::pair<irep_idt, unsigned>, std::optional<unsigned>>;
70 std::string loop_limit,
74 #define OPT_UNWINDSET \
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"
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.
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)
void parse_unwind(const std::string &unwind)
std::map< std::pair< irep_idt, unsigned >, std::optional< unsigned > > thread_loop_mapt
std::optional< unsigned > global_limit
thread_loop_mapt thread_loop_map
unwindsett(abstract_goto_modelt &goto_model)
void parse_unwindset_file(const std::string &file_name, message_handlert &message_handler)
abstract_goto_modelt & goto_model
std::map< irep_idt, std::optional< unsigned > > loop_mapt
void parse_unwindset(const std::list< std::string > &unwindset, message_handlert &message_handler)
const std::string thread_id