CBMC
remove_skip.cpp File Reference

Program Transformation. More...

#include "remove_skip.h"
#include "goto_model.h"
#include <util/std_code.h>
+ Include dependency graph for remove_skip.cpp:

Go to the source code of this file.

Functions

bool is_skip (const goto_programt &body, goto_programt::const_targett it, bool ignore_labels)
 Determine whether the instruction is semantically equivalent to a skip (no-op). More...
 
void remove_skip (goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
 remove unnecessary skip statements More...
 
void remove_skip (goto_programt &goto_program)
 remove unnecessary skip statements More...
 
void remove_skip (goto_functionst &goto_functions)
 remove unnecessary skip statements More...
 
void remove_skip (goto_modelt &goto_model)
 

Detailed Description

Program Transformation.

Definition in file remove_skip.cpp.

Function Documentation

◆ is_skip()

bool is_skip ( const goto_programt body,
goto_programt::const_targett  it,
bool  ignore_labels 
)

Determine whether the instruction is semantically equivalent to a skip (no-op).

This includes a skip, but also if(false) goto ..., goto next; next: ..., and (void)0.

Parameters
bodygoto program containing the instruction
itinstruction iterator that is tested for being a skip (or equivalent)
ignore_labelsIf the caller takes care of moving labels, then even skip statements carrying labels can be treated as skips (even though they may carry key information such as error labels).
Returns
True, iff it is equivalent to a skip.

Definition at line 27 of file remove_skip.cpp.

◆ remove_skip() [1/4]

void remove_skip ( goto_functionst goto_functions)

remove unnecessary skip statements

Definition at line 199 of file remove_skip.cpp.

◆ remove_skip() [2/4]

void remove_skip ( goto_modelt goto_model)

Definition at line 213 of file remove_skip.cpp.

◆ remove_skip() [3/4]

void remove_skip ( goto_programt goto_program)

remove unnecessary skip statements

Definition at line 188 of file remove_skip.cpp.

◆ remove_skip() [4/4]

void remove_skip ( goto_programt goto_program,
goto_programt::targett  begin,
goto_programt::targett  end 
)

remove unnecessary skip statements

Parameters
goto_programgoto program containing the instructions to be cleaned in the range [begin, end)
beginiterator pointing to first instruction to be considered
enditerator pointing beyond last instruction to be considered

Definition at line 87 of file remove_skip.cpp.