#include <goto_contractor.h>

Inheritance diagram for goto_contractort:

Public Member Functions
void	goto_contractor_condition (const namespacet &namespacet, const optionst &optionst)
	goto_contractort (goto_functionst &_goto_functions, const namespacet &ns, const optionst &options)
	This constructor will run the goto-contractor procedure.
Public Member Functions inherited from goto_functions_algorithm
	goto_functions_algorithm (bool sideffect)
unsigned	get_number_of_functions ()
unsigned	get_number_of_loops ()
bool	run (goto_functionst &) override
	Executes the algorithm over a T object.
void	setTarget (const std::string &_tgt)
Public Member Functions inherited from algorithm< goto_functionst >
	algorithm (bool sideeffect)
virtual	~algorithm ()=default
bool	has_sideeffect ()
	Says wether the algorithm is a plain analysis or if it also changes the structure.

Protected Attributes
goto_functionst &	goto_functions
Protected Attributes inherited from goto_functions_algorithm
std::string	target_function = ""
Protected Attributes inherited from algorithm< goto_functionst >
const bool	sideeffect

Additional Inherited Members
Protected Member Functions inherited from goto_functions_algorithm
virtual bool	runOnFunction (std::pair< const irep_idt, goto_functiont > &F)
virtual bool	runOnLoop (loopst &loop, goto_programt &goto_program)
virtual bool	runOnProgram (goto_functionst &)

Constructor & Destructor Documentation

◆ goto_contractort()

goto_contractort::goto_contractort	(	goto_functionst &	_goto_functions,
		const namespacet &	ns,
		const optionst &	options )

inline

This constructor will run the goto-contractor procedure.

it will go through 4 steps. First is parsing the properties. Second, parsing the intervals. Third, applying the contractor. Fourth, inserting assumes in the program to reflect the contracted intervals.

Parameters

_goto_functions

Member Function Documentation

◆ goto_contractor_condition()

void goto_contractort::goto_contractor_condition	(	const namespacet &	namespacet,
		const optionst &	optionst )

Member Data Documentation

◆ goto_functions

goto_functionst& goto_contractort::goto_functions

protected

The documentation for this class was generated from the following files:

src/goto-programs/goto_contractor.h
src/goto-programs/goto_contractor.cpp

Public Member Functions