CBMC
Loading...
Searching...
No Matches
remove_skip.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Program Transformation
4
5Author: 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
17class goto_functionst;
18class goto_modelt;
19
20bool is_skip(
21 const goto_programt &,
23 bool ignore_labels = false);
27
28void remove_skip(
29 goto_programt &goto_program,
31 const goto_programt::targett end);
32
33#endif // CPROVER_GOTO_PROGRAMS_REMOVE_SKIP_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
A collection of goto functions.
A generic container class for the GOTO intermediate representation of one function.
instructionst::iterator targett
instructionst::const_iterator const_targett
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).
void remove_skip(goto_programt &)
remove unnecessary skip statements