This transformation detects whether the unroll intrinsic was used and then mark the loop with the specific unwind. More...

#include <loop_unroll.h>

Inheritance diagram for apply_intrinsic_unroller:

[legend]

Public Member Functions
	apply_intrinsic_unroller ()
bool	run (goto_functionst &goto_functions) override
	Executes the algorithm over a T object.
Public Member Functions inherited from goto_functions_algorithm
	goto_functions_algorithm (bool sideffect)
unsigned	get_number_of_functions ()
unsigned	get_number_of_loops ()
bool	run (goto_functionst &) override
	Executes the algorithm over a T object.
void	setTarget (const std::string &_tgt)
Public Member Functions inherited from algorithm< goto_functionst >
	algorithm (bool sideeffect)
virtual	~algorithm ()=default
bool	has_sideeffect ()
	Says wether the algorithm is a plain analysis or if it also changes the structure.

Protected Member Functions
bool	runOnLoop (loopst &loop, goto_programt &goto_program) override
Protected Member Functions inherited from goto_functions_algorithm
virtual bool	runOnFunction (std::pair< const irep_idt, goto_functiont > &F)
virtual bool	runOnProgram (goto_functionst &)

Additional Inherited Members
Protected Attributes inherited from goto_functions_algorithm
std::string	target_function = ""
Protected Attributes inherited from algorithm< goto_functionst >
const bool	sideeffect

Detailed Description

This transformation detects whether the unroll intrinsic was used and then mark the loop with the specific unwind.

__ESBMC_unroll(4); for(int i = 0; i < 4; i++)

vvvvv

FUNCTION_CALL __ESBMC_unroll(N) DECL i i = 0 1: ...

We want to automatically set the next loop unwinding to 4.

The intrinsic is bound to the loop whose head immediately follows it, skipping over the loop preamble (variable declarations, initialisers and condition side-effects such as while (int v = f())). Any __ESBMC_unroll call that is not directly followed by a loop is reported as misplaced.

Constructor & Destructor Documentation

◆ apply_intrinsic_unroller()

apply_intrinsic_unroller::apply_intrinsic_unroller ( )

inline

Member Function Documentation

◆ run()

bool apply_intrinsic_unroller::run ( goto_functionst & )

overridevirtual

Executes the algorithm over a T object.

Returns: success of the algorithm

Implements algorithm< goto_functionst >.

◆ runOnLoop()

bool apply_intrinsic_unroller::runOnLoop	(	loopst &	loop,
		goto_programt &	goto_program )

overrideprotectedvirtual

Reimplemented from goto_functions_algorithm.

The documentation for this class was generated from the following files:

src/goto-programs/loop_unroll.h
src/goto-programs/loop_unroll.cpp

Public Member Functions