cprover
|
Skip over selected loops by adding gotos. More...
#include "skip_loops.h"
#include <util/message.h>
#include <util/string2int.h>
#include <goto-programs/goto_functions.h>
Go to the source code of this file.
Typedefs | |
typedef std::set< unsigned > | loop_idst |
typedef std::map< irep_idt, loop_idst > | loop_mapt |
Functions | |
static bool | skip_loops (goto_programt &goto_program, const loop_idst &loop_ids, messaget &message) |
static bool | parse_loop_ids (const std::string &loop_ids, loop_mapt &loop_map) |
bool | skip_loops (goto_functionst &goto_functions, const std::string &loop_ids, message_handlert &message_handler) |
Skip over selected loops by adding gotos.
Definition in file skip_loops.cpp.
typedef std::set<unsigned> loop_idst |
Definition at line 21 of file skip_loops.cpp.
Definition at line 22 of file skip_loops.cpp.
|
static |
Definition at line 65 of file skip_loops.cpp.
References irept::find(), safe_string2unsigned(), and size_type().
Referenced by skip_loops().
|
static |
Definition at line 24 of file skip_loops.cpp.
References messaget::eom(), messaget::error(), Forall_goto_program_instructions, goto_program_templatet< codeT, guardT >::insert_before(), and goto_program_templatet< codeT, guardT >::instructions.
Referenced by goto_instrument_parse_optionst::instrument_goto_program(), and skip_loops().
bool skip_loops | ( | goto_functionst & | goto_functions, |
const std::string & | loop_ids, | ||
message_handlert & | message_handler | ||
) |
Definition at line 93 of file skip_loops.cpp.
References messaget::eom(), messaget::error(), Forall_goto_functions, parse_loop_ids(), skip_loops(), and goto_functions_templatet< bodyT >::update().