remove_skip.h File Reference

#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
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). More...
void	remove_skip (goto_programt &)
	remove unnecessary skip statements More...
void	remove_skip (goto_functionst &)
	remove unnecessary skip statements More...
void	remove_skip (goto_modelt &)
void	remove_skip (goto_programt &goto_program, goto_programt::targett begin, const goto_programt::targett end)
	remove unnecessary skip statements More...

Detailed Description

Program Transformation

Definition in file remove_skip.h.

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

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_functionst &

)

remove unnecessary skip statements

Definition at line 196 of file remove_skip.cpp.

remove_skip() [2/4]

void remove_skip

(

goto_modelt &

)

Definition at line 210 of file remove_skip.cpp.

remove_skip() [3/4]

void remove_skip

(

goto_programt &

)

remove unnecessary skip statements

Definition at line 185 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_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.