k_induction.cpp File Reference

k-induction More...

#include "k_induction.h"
#include <util/std_expr.h>
#include <analyses/natural_loops.h>
#include <analyses/local_may_alias.h>
#include <goto-programs/remove_skip.h>
#include "unwind.h"
#include "loop_utils.h"

Include dependency graph for k_induction.cpp:

Go to the source code of this file.

Classes
class	k_inductiont

Functions
void	k_induction (goto_functionst &goto_functions, bool base_case, bool step_case, unsigned k)

Detailed Description

k-induction

Definition in file k_induction.cpp.

Function Documentation

k_induction()

void k_induction	(	goto_functionst &	goto_functions,
		bool	base_case,
		bool	step_case,
		unsigned	k
	)

Definition at line 152 of file k_induction.cpp.

References Forall_goto_functions.

Referenced by goto_instrument_parse_optionst::instrument_goto_program().