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 &,
22  goto_programt::const_targett,
23  bool ignore_labels = false);
24 void remove_skip(goto_programt &);
25 void remove_skip(goto_functionst &);
26 void remove_skip(goto_modelt &);
27 
28 void remove_skip(
29  goto_programt &goto_program,
30  goto_programt::targett begin,
31  const goto_programt::targett end);
32 
33 #endif // CPROVER_GOTO_PROGRAMS_REMOVE_SKIP_H
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:25
goto_modelt
Definition: goto_model.h:27
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:614
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:615
goto_program.h
Concrete Goto Program.
is_skip
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
remove_skip
void remove_skip(goto_programt &)
remove unnecessary skip statements
Definition: remove_skip.cpp:188