assign_params_as_non_det Class Reference

To make the counterexample trace complete in "--function" mode. More...

#include <assign_params_as_non_det.h>

Inheritance diagram for assign_params_as_non_det:

Public Member Functions
	assign_params_as_non_det (contextt &context)
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 Member Functions
virtual bool	runOnFunction (std::pair< const irep_idt, goto_functiont > &F) override
symbolt *	get_default_symbol (typet type, std::string name, std::string id, locationt location)
Protected Member Functions inherited from goto_functions_algorithm
virtual bool	runOnLoop (loopst &loop, goto_programt &goto_program)
virtual bool	runOnProgram (goto_functionst &)

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

Detailed Description

To make the counterexample trace complete in "--function" mode.

Constructor & Destructor Documentation

assign_params_as_non_det()

assign_params_as_non_det::assign_params_as_non_det ( contextt & context )

inline

Member Function Documentation

get_default_symbol()

symbolt * assign_params_as_non_det::get_default_symbol ( typet type, std::string name, std::string id, locationt location )

protected

runOnFunction()

bool assign_params_as_non_det::runOnFunction ( std::pair< const irep_idt, goto_functiont > & F )

overrideprotectedvirtual

hack: we use !flag (forward jump over the body) so the condition is not counted in goto_coverage.

Reimplemented from goto_functions_algorithm.

Member Data Documentation

context

contextt& assign_params_as_non_det::context

protected

---

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

• src/goto-programs/assign_params_as_non_det.h
• src/goto-programs/assign_params_as_non_det.cpp