#include <goto_diff.h>

Inheritance diagram for goto_difft:

Collaboration diagram for goto_difft:

Public Member Functions
	goto_difft (const goto_modelt &_goto_model1, const goto_modelt &_goto_model2, const optionst &_options, ui_message_handlert &_message_handler)

virtual	~goto_difft ()=default

virtual bool	operator() ()=0

virtual void	output_functions () const
	Output diff result. More...

Protected Member Functions
void	output_function_group (const std::string &group_name, const std::set< irep_idt > &function_group, const goto_modelt &goto_model) const
	Output group of functions in plain text format. More...

void	output_function (const irep_idt &function_name, const goto_modelt &goto_model) const
	Output function information in plain text format. More...

void	convert_function_group_json (json_arrayt &result, const std::set< irep_idt > &function_group, const goto_modelt &goto_model) const
	Convert a function group to JSON. More...

void	convert_function_json (json_objectt &result, const irep_idt &function_name, const goto_modelt &goto_model) const
	Convert function information to JSON. More...

Protected Attributes
ui_message_handlert &	message_handler

const goto_modelt &	goto_model1

const goto_modelt &	goto_model2

const optionst &	options

unsigned	total_functions_count

std::set< irep_idt >	new_functions

std::set< irep_idt >	modified_functions

std::set< irep_idt >	deleted_functions

Detailed Description

Definition at line 25 of file goto_diff.h.

Constructor & Destructor Documentation

◆ goto_difft()

goto_difft::goto_difft	(	const goto_modelt &	_goto_model1,
		const goto_modelt &	_goto_model2,
		const optionst &	_options,
		ui_message_handlert &	_message_handler
	)

inline

Definition at line 28 of file goto_diff.h.

◆ ~goto_difft()

virtual goto_difft::~goto_difft ( )

virtualdefault

Member Function Documentation

◆ convert_function_group_json()

void goto_difft::convert_function_group_json	(	json_arrayt &	result,
		const std::set< irep_idt > &	function_group,
		const goto_modelt &	goto_model
	)		const

protected

Convert a function group to JSON.

Parameters

result	the JSON array to be populated
function_group	set of function ids in the group
goto_model	the goto model

Definition at line 120 of file goto_diff_base.cpp.

◆ convert_function_json()

void goto_difft::convert_function_json	(	json_objectt &	result,
		const irep_idt &	function_name,
		const goto_modelt &	goto_model
	)		const

protected

Convert function information to JSON.

Parameters

result	the JSON object to be populated
function_name	the function id
goto_model	the goto model

Definition at line 136 of file goto_diff_base.cpp.

◆ operator()()

virtual bool goto_difft::operator() ( )

pure virtual

Implemented in syntactic_difft, and java_syntactic_difft.

◆ output_function()

void goto_difft::output_function	(	const irep_idt &	function_name,
		const goto_modelt &	goto_model
	)		const

protected

Output function information in plain text format.

Parameters

function_name	the function id
goto_model	the goto model

Definition at line 83 of file goto_diff_base.cpp.

◆ output_function_group()

void goto_difft::output_function_group	(	const std::string &	group_name,
		const std::set< irep_idt > &	function_group,
		const goto_modelt &	goto_model
	)		const

protected

Output group of functions in plain text format.

Parameters

group_name	the name of the group, e.g. "modified functions"
function_group	set of function ids in the group
goto_model	the goto model

Definition at line 68 of file goto_diff_base.cpp.

◆ output_functions()

void goto_difft::output_functions ( ) const

virtual

Output diff result.

Definition at line 21 of file goto_diff_base.cpp.

Member Data Documentation

◆ deleted_functions

std::set<irep_idt> goto_difft::deleted_functions

protected

Definition at line 54 of file goto_diff.h.

◆ goto_model1

const goto_modelt& goto_difft::goto_model1

protected

Definition at line 49 of file goto_diff.h.

◆ goto_model2

const goto_modelt& goto_difft::goto_model2

protected

Definition at line 50 of file goto_diff.h.

◆ message_handler

ui_message_handlert& goto_difft::message_handler

protected

Definition at line 48 of file goto_diff.h.

◆ modified_functions

std::set<irep_idt> goto_difft::modified_functions

protected

Definition at line 54 of file goto_diff.h.

◆ new_functions

std::set<irep_idt> goto_difft::new_functions

protected

Definition at line 54 of file goto_diff.h.

◆ options

const optionst& goto_difft::options

protected

Definition at line 51 of file goto_diff.h.

◆ total_functions_count

unsigned goto_difft::total_functions_count

protected

Definition at line 53 of file goto_diff.h.

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

/home/runner/work/cbmc/cbmc/src/goto-diff/goto_diff.h
/home/runner/work/cbmc/cbmc/src/goto-diff/goto_diff_base.cpp

Public Member Functions

Protected Member Functions

Protected Attributes

Detailed Description

Constructor & Destructor Documentation

◆ goto_difft()

◆ ~goto_difft()

Member Function Documentation

◆ convert_function_group_json()

◆ convert_function_json()

◆ operator()()

◆ output_function()

◆ output_function_group()

◆ output_functions()

Member Data Documentation

◆ deleted_functions

◆ goto_model1

◆ goto_model2

◆ message_handler

◆ modified_functions

◆ new_functions

◆ options

◆ total_functions_count