cprover
|
#include <goto_diff.h>
Public Member Functions | |
goto_difft (const goto_modelt &_goto_model1, const goto_modelt &_goto_model2, const optionst &_options, message_handlert &_message_handler) | |
virtual bool | operator() ()=0 |
void | set_ui (ui_message_handlert::uit _ui) |
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 | |
const goto_modelt & | goto_model1 |
const goto_modelt & | goto_model2 |
const optionst & | options |
ui_message_handlert::uit | ui |
unsigned | total_functions_count |
std::set< irep_idt > | new_functions |
std::set< irep_idt > | modified_functions |
std::set< irep_idt > | deleted_functions |
Additional Inherited Members |
Definition at line 25 of file goto_diff.h.
|
inline |
Definition at line 28 of file goto_diff.h.
|
protected |
Convert a function group to JSON.
result | the JSON array to be populated |
function_group | set of function ids in the group |
goto_model | the goto model |
Definition at line 115 of file goto_diff_base.cpp.
References convert_function_json(), and messaget::result().
Referenced by output_functions().
|
protected |
Convert function information to JSON.
result | the JSON object to be populated |
function_name | the function id |
goto_model | the goto model |
Definition at line 131 of file goto_diff_base.cpp.
References CHECK_RETURN, convert_properties_json(), goto_functionst::function_map, optionst::get_bool_option(), goto_modelt::goto_functions, goto_program, json(), symbolt::location, namespacet::lookup(), options, messaget::result(), and goto_modelt::symbol_table.
Referenced by convert_function_group_json().
|
pure virtual |
Implemented in syntactic_difft, and java_syntactic_difft.
|
protected |
Output function information in plain text format.
function_name | the function id |
goto_model | the goto model |
Definition at line 81 of file goto_diff_base.cpp.
References CHECK_RETURN, goto_functionst::function_map, optionst::get_bool_option(), source_locationt::get_file(), source_locationt::get_property_id(), goto_modelt::goto_functions, goto_program, goto_programt::instructions, symbolt::location, namespacet::lookup(), options, messaget::result(), and goto_modelt::symbol_table.
Referenced by output_function_group().
|
protected |
Output group of functions in plain text format.
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 66 of file goto_diff_base.cpp.
References output_function(), and messaget::result().
Referenced by output_functions().
|
virtual |
Output diff result.
Definition at line 21 of file goto_diff_base.cpp.
References convert_function_group_json(), deleted_functions, messaget::eom(), messaget::error(), goto_model1, goto_model2, ui_message_handlert::JSON_UI, modified_functions, new_functions, output_function_group(), ui_message_handlert::PLAIN, messaget::result(), to_string(), total_functions_count, ui, and ui_message_handlert::XML_UI.
Referenced by jdiff_parse_optionst::doit(), and goto_diff_parse_optionst::doit().
|
inline |
Definition at line 44 of file goto_diff.h.
References ui.
Referenced by jdiff_parse_optionst::doit(), and goto_diff_parse_optionst::doit().
|
protected |
Definition at line 55 of file goto_diff.h.
Referenced by java_syntactic_difft::operator()(), syntactic_difft::operator()(), and output_functions().
|
protected |
Definition at line 49 of file goto_diff.h.
Referenced by java_syntactic_difft::operator()(), syntactic_difft::operator()(), and output_functions().
|
protected |
Definition at line 50 of file goto_diff.h.
Referenced by java_syntactic_difft::operator()(), syntactic_difft::operator()(), and output_functions().
|
protected |
Definition at line 55 of file goto_diff.h.
Referenced by java_syntactic_difft::operator()(), syntactic_difft::operator()(), and output_functions().
|
protected |
Definition at line 55 of file goto_diff.h.
Referenced by java_syntactic_difft::operator()(), syntactic_difft::operator()(), and output_functions().
|
protected |
Definition at line 51 of file goto_diff.h.
Referenced by convert_function_json(), and output_function().
|
protected |
Definition at line 54 of file goto_diff.h.
Referenced by java_syntactic_difft::operator()(), syntactic_difft::operator()(), and output_functions().
|
protected |
Definition at line 52 of file goto_diff.h.
Referenced by output_functions(), and set_ui().