inductiveness.h File Reference

Inductiveness. More...

#include "solver_types.h"

Include dependency graph for inductiveness.h:

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

Go to the source code of this file.

Classes
class	inductiveness_resultt

Functions
inductiveness_resultt	inductiveness_check (std::vector< framet > &frames, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const solver_optionst &, const namespacet &, std::vector< propertyt > &properties, std::size_t property_index)

Detailed Description

Inductiveness.

Definition in file inductiveness.h.

Function Documentation

inductiveness_check()

inductiveness_resultt inductiveness_check	(	std::vector< framet > &	frames,
		const std::unordered_set< symbol_exprt, irep_hash > &	address_taken,
		const solver_optionst &	solver_options,
		const namespacet &	ns,
		std::vector< propertyt > &	properties,
		std::size_t	property_index
	)

Definition at line 98 of file inductiveness.cpp.