CBMC
Loading...
Searching...
No Matches
Functions
remove_skip.h File Reference

Program Transformation. More...

#include "goto_program.h"
+ Include dependency graph for remove_skip.h:
+ This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Functions

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

Detailed Description

Program Transformation.

Definition in file remove_skip.h.

Function Documentation

◆  is_skip()

bool is_skip ( const goto_programtbody,
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
body goto program containing the instruction
it instruction iterator that is tested for being a skip (or equivalent)
ignore_labels If 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_functionstgoto_functions )

remove unnecessary skip statements

Definition at line 199 of file remove_skip.cpp.

◆  remove_skip() [2/4]

void remove_skip ( goto_modeltgoto_model )

Definition at line 213 of file remove_skip.cpp.

◆  remove_skip() [3/4]

void remove_skip ( goto_programtgoto_program )

remove unnecessary skip statements

Definition at line 188 of file remove_skip.cpp.

◆  remove_skip() [4/4]

void remove_skip ( goto_programtgoto_program,
)

remove unnecessary skip statements

Parameters
goto_program goto program containing the instructions to be cleaned in the range [begin, end)
begin iterator pointing to first instruction to be considered
end iterator pointing beyond last instruction to be considered

Definition at line 87 of file remove_skip.cpp.

AltStyle によって変換されたページ (->オリジナル) /