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 >	modifiest
typedef const natural_loops_mutablet::natural_loopt	loopt

Functions
void	get_modifies (const local_may_aliast &local_may_alias, const loopt &loop, modifiest &modifies)
void	build_havoc_code (const goto_programt::targett loop_head, const modifiest &modifies, goto_programt &dest)
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

loopt

typedef const natural_loops_mutablet::natural_loopt loopt

Definition at line 20 of file loop_utils.h.

modifiest

typedef std::set<exprt> modifiest

Definition at line 17 of file loop_utils.h.

Function Documentation

build_havoc_code()

void build_havoc_code	(	const goto_programt::targett	loop_head,
		const modifiest &	modifies,
		goto_programt &	dest
	)

Definition at line 37 of file loop_utils.cpp.

get_loop_exit()

goto_programt::targett get_loop_exit

(

const loopt &

)

get_modifies()

void get_modifies	(	const local_may_aliast &	local_may_alias,
		const loopt &	loop,
		modifiest &	modifies
	)