loop_utils.h File Reference

Helper functions for k-induction and loop invariants. More...

#include <analyses/natural_loops.h>

Include dependency graph for loop_utils.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Typedefs
typedef std::set< exprt >	assignst
typedef natural_loops_mutablet::natural_loopt	loopt

Functions
void	get_assigns (const local_may_aliast &local_may_alias, const loopt &loop, assignst &assigns)
void	get_assigns (const local_may_aliast &local_may_alias, const loopt &loop, assignst &assigns, std::function< bool(const exprt &)> predicate)
	get all assign targets that satisfy predicate within the loops. More...
void	get_assigns_lhs (const local_may_aliast &local_may_alias, goto_programt::const_targett t, const exprt &lhs, assignst &assigns)
void	get_assigns_lhs (const local_may_aliast &local_may_alias, goto_programt::const_targett t, const exprt &lhs, assignst &assigns, std::function< bool(const exprt &)> predicate)
	get all assign targets that satisfy predicate from lhs. More...
goto_programt::targett	get_loop_exit (const loopt &)

Detailed Description

Helper functions for k-induction and loop invariants.

Definition in file loop_utils.h.

Typedef Documentation

assignst

typedef std::set<exprt> assignst

Definition at line 19 of file loop_utils.h.

loopt

typedef natural_loops_mutablet::natural_loopt loopt

Definition at line 20 of file loop_utils.h.

Function Documentation

get_assigns() [1/2]

void get_assigns	(	const local_may_aliast &	local_may_alias,
		const loopt &	loop,
		assignst &	assigns
	)

Definition at line 142 of file loop_utils.cpp.

get_assigns() [2/2]

void get_assigns	(	const local_may_aliast &	local_may_alias,
		const loopt &	loop,
		assignst &	assigns,
		std::function< bool(const exprt &)>	predicate
	)

get all assign targets that satisfy predicate within the loops.

Definition at line 151 of file loop_utils.cpp.

get_assigns_lhs() [1/2]

void get_assigns_lhs	(	const local_may_aliast &	local_may_alias,
		goto_programt::const_targett	t,
		const exprt &	lhs,
		assignst &	assigns
	)

Definition at line 39 of file loop_utils.cpp.

get_assigns_lhs() [2/2]

void get_assigns_lhs	(	const local_may_aliast &	local_may_alias,
		goto_programt::const_targett	t,
		const exprt &	lhs,
		assignst &	assigns,
		std::function< bool(const exprt &)>	predicate
	)

get all assign targets that satisfy predicate from lhs.

Definition at line 49 of file loop_utils.cpp.

get_loop_exit()

goto_programt::targett get_loop_exit

(

const loopt &

loop

)

Definition at line 21 of file loop_utils.cpp.