loop_utils.cpp File Reference

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

#include "loop_utils.h"
#include <util/std_expr.h>
#include <analyses/natural_loops.h>
#include <analyses/local_may_alias.h>

Include dependency graph for loop_utils.cpp:

Go to the source code of this file.

Functions
goto_programt::targett	get_loop_exit (const loopt &loop)
void	build_havoc_code (const goto_programt::targett loop_head, const modifiest &modifies, goto_programt &dest)
static void	get_modifies_lhs (const local_may_aliast &local_may_alias, goto_programt::const_targett t, const exprt &lhs, modifiest &modifies)
void	get_modifies (const local_may_aliast &local_may_alias, const loopt &loop, modifiest &modifies)

Detailed Description

Helper functions for k-induction and loop invariants.

Definition in file loop_utils.cpp.

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 &

loop

)

Definition at line 19 of file loop_utils.cpp.

get_modifies()

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

Definition at line 89 of file loop_utils.cpp.

get_modifies_lhs()

static void get_modifies_lhs ( const local_may_aliast &  local_may_alias, goto_programt::const_targett  t, const exprt &  lhs, modifiest &  modifies  )

static

Definition at line 59 of file loop_utils.cpp.