cbmc/remove__skip_8h_source.html

/*******************************************************************\


Module: Program Transformation


Author: Daniel Kroening, kroening@kroening.com


\*******************************************************************/


#ifndef CPROVER_GOTO_PROGRAMS_REMOVE_SKIP_H

#define CPROVER_GOTO_PROGRAMS_REMOVE_SKIP_H


#include "goto_program.h"


class goto_functionst;

class goto_modelt;


bool is_skip(

  const goto_programt &,

  goto_programt::const_targett,

  bool ignore_labels = false);

void remove_skip(goto_programt &);

void remove_skip(goto_functionst &);

void remove_skip(goto_modelt &);


void remove_skip(

  goto_programt &goto_program,

  goto_programt::targett begin,

  const goto_programt::targett end);


#endif // CPROVER_GOTO_PROGRAMS_REMOVE_SKIP_H

ait
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562

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