CBMC
remove_skip.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Program Transformation
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_GOTO_PROGRAMS_REMOVE_SKIP_H
13 #define CPROVER_GOTO_PROGRAMS_REMOVE_SKIP_H
14 
15 #include "goto_program.h"
16 
17 class goto_functionst;
18 class goto_modelt;
19 
20 bool is_skip(
21  const goto_programt &,
23  bool ignore_labels = false);
26 void remove_skip(goto_modelt &);
27 
28 void remove_skip(
29  goto_programt &goto_program,
31  const goto_programt::targett end);
32 
33 #endif // CPROVER_GOTO_PROGRAMS_REMOVE_SKIP_H
A collection of goto functions.
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
instructionst::iterator targett
Definition: goto_program.h:614
instructionst::const_iterator const_targett
Definition: goto_program.h:615
Concrete Goto Program.
bool is_skip(const goto_programt &, goto_programt::const_targett, bool ignore_labels=false)
Determine whether the instruction is semantically equivalent to a skip (no-op).
Definition: remove_skip.cpp:27
void remove_skip(goto_programt &)
remove unnecessary skip statements