Loading...

Searching...

No Matches

goto_diff_base.cpp

Go to the documentation of this file.

1/*******************************************************************\

2

3Module: GOTO-DIFF Base Class

4

5Author: Peter Schrammel

6

7\*******************************************************************/

8

11

12#include "goto_diff.h"

13

14#include <util/json_irep.h>

15#include <util/options.h>

16

17#include <goto-programs/goto_model.h>

18#include <goto-programs/show_properties.h>

19

21 void goto_difft::output_functions() const

22{

23 messaget msg(message_handler);

24

25 switch(message_handler.get_ui())

26 {

27 case ui_message_handlert::uit::PLAIN:

28 {

29 msg.result() << "total number of functions: " << total_functions_count

30 << '\n' << messaget::eom;

31 output_function_group("new functions", new_functions, goto_model2);

32 output_function_group(

33 "modified functions", modified_functions, goto_model2);

34 output_function_group(

35 "deleted functions", deleted_functions, goto_model1);

36 msg.result() << messaget::eom;

37 break;

38 }

39 case ui_message_handlert::uit::JSON_UI:

40 {

41 json_objectt json_result{

42 {"totalNumberOfFunctions",

43 json_stringt(std::to_string(total_functions_count))}};

44 convert_function_group_json(

45 json_result["newFunctions"].make_array(), new_functions, goto_model2);

46 convert_function_group_json(

47 json_result["modifiedFunctions"].make_array(),

48 modified_functions,

49 goto_model2);

50 convert_function_group_json(

51 json_result["deletedFunctions"].make_array(),

52 deleted_functions,

53 goto_model1);

54 msg.result() << json_result << messaget::eom;

55 break;

56 }

57 case ui_message_handlert::uit::XML_UI:

58 {

59 msg.error() << "XML output not supported yet" << messaget::eom;

60 break;

61 }

62 }

63}

64

69 void goto_difft::output_function_group(

70 const std::string &group_name,

71 const std::set<irep_idt> &function_group,

72 const goto_modelt &goto_model) const

73{

74 messaget(message_handler).result() << group_name << ':' << messaget::eom;

75 for(const auto &function_name : function_group)

76 {

77 output_function(function_name, goto_model);

78 }

79}

80

84 void goto_difft::output_function(

85 const irep_idt &function_name,

86 const goto_modelt &goto_model) const

87{

88 messaget msg(message_handler);

89

90 namespacet ns(goto_model.symbol_table);

91 const symbolt &symbol = ns.lookup(function_name);

92

93 msg.result() << " " << symbol.location.get_file() << ": " << function_name;

94

95 if(options.get_bool_option("show-properties"))

96 {

97 const auto goto_function_it =

98 goto_model.goto_functions.function_map.find(function_name);

99 CHECK_RETURN(

100 goto_function_it != goto_model.goto_functions.function_map.end());

101 const goto_programt &goto_program = goto_function_it->second.body;

102

103 for(const auto &ins : goto_program.instructions)

104 {

105 if(!ins.is_assert())

106 continue;

107

108 const source_locationt &source_location = ins.source_location();

109 irep_idt property_id = source_location.get_property_id();

110 msg.result() << "\n " << property_id;

111 }

112 }

113

114 msg.result() << messaget::eom;

115}

116

121 void goto_difft::convert_function_group_json(

122 json_arrayt &result,

123 const std::set<irep_idt> &function_group,

124 const goto_modelt &goto_model) const

125{

126 for(const auto &function_name : function_group)

127 {

128 convert_function_json(

129 result.push_back(jsont()).make_object(), function_name, goto_model);

130 }

131}

132

137 void goto_difft::convert_function_json(

138 json_objectt &result,

139 const irep_idt &function_name,

140 const goto_modelt &goto_model) const

141{

142 namespacet ns(goto_model.symbol_table);

143 const symbolt &symbol = ns.lookup(function_name);

144

145 result["name"] = json_stringt(function_name);

146 result["sourceLocation"] = json(symbol.location);

147

148 if(options.get_bool_option("show-properties"))

149 {

150 const auto goto_function_it =

151 goto_model.goto_functions.function_map.find(function_name);

152 CHECK_RETURN(

153 goto_function_it != goto_model.goto_functions.function_map.end());

154 const goto_programt &goto_program = goto_function_it->second.body;

155

156 convert_properties_json(

157 result["properties"].make_array(), ns, function_name, goto_program);

158 }

159}

ait

ait supplies three of the four components needed: an abstract interpreter (in this case handling func...

Definition ai.h:566

dstringt

dstringt has one field, an unsigned integer no which is an index into a static table of strings.

Definition dstring.h:38

goto_difft::options

const optionst & options

Definition goto_diff.h:51

goto_difft::output_function

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

Output function information in plain text format.

Definition goto_diff_base.cpp:84

goto_difft::modified_functions

std::set< irep_idt > modified_functions

Definition goto_diff.h:54

goto_difft::convert_function_group_json

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.

Definition goto_diff_base.cpp:121

goto_difft::goto_model1

const goto_modelt & goto_model1

Definition goto_diff.h:49

goto_difft::output_functions

virtual void output_functions() const

Output diff result.

Definition goto_diff_base.cpp:21

goto_difft::convert_function_json

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

Convert function information to JSON.

Definition goto_diff_base.cpp:137

goto_difft::new_functions

std::set< irep_idt > new_functions

Definition goto_diff.h:54

goto_difft::output_function_group

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.

Definition goto_diff_base.cpp:69

goto_difft::total_functions_count

unsigned total_functions_count

Definition goto_diff.h:53

goto_difft::deleted_functions

std::set< irep_idt > deleted_functions

Definition goto_diff.h:54

goto_difft::goto_model2

const goto_modelt & goto_model2

Definition goto_diff.h:50

goto_difft::message_handler

ui_message_handlert & message_handler

Definition goto_diff.h:48

goto_functionst::function_map

function_mapt function_map

Definition goto_functions.h:29

goto_modelt

Definition goto_model.h:27

goto_modelt::symbol_table

symbol_tablet symbol_table

Symbol table.

Definition goto_model.h:31

goto_modelt::goto_functions

goto_functionst goto_functions

GOTO functions.

Definition goto_model.h:34

goto_programt

A generic container class for the GOTO intermediate representation of one function.

Definition goto_program.h:72

goto_programt::instructions

instructionst instructions

The list of instructions in the goto program.

Definition goto_program.h:621

json_arrayt

Definition json.h:165

json_arrayt::push_back

jsont & push_back(const jsont &json)

Definition json.h:212

json_objectt

Definition json.h:298

json_stringt

Definition json.h:270

jsont

Definition json.h:27

messaget

Class that provides messages with a built-in verbosity 'level'.

Definition message.h:154

messaget::result

mstreamt & result() const

Definition message.h:411

messaget::eom

static eomt eom

Definition message.h:289

namespacet

A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...

Definition namespace.h:91

namespacet::lookup

bool lookup(const irep_idt &name, const symbolt *&symbol) const override

See documentation for namespace_baset::lookup().

Definition namespace.cpp:134

source_locationt

Definition source_location.h:20

source_locationt::get_property_id

const irep_idt & get_property_id() const

Definition source_location.h:69

source_locationt::get_file

const irep_idt & get_file() const

Definition source_location.h:36

symbolt

Symbol table entry.

Definition symbol.h:28

symbolt::location

source_locationt location

Source code location of definition of symbol.

Definition symbol.h:37

ui_message_handlert::get_ui

virtual uit get_ui() const

Definition ui_message.h:33

ui_message_handlert::uit::JSON_UI

@ JSON_UI

ui_message_handlert::uit::XML_UI

@ XML_UI

ui_message_handlert::uit::PLAIN

@ PLAIN

goto_diff.h

GOTO-DIFF Base Class.

Symbol Table + CFG.

Util.

Options.

static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)

Definition properties.cpp:120

convert_properties_json

void convert_properties_json(json_arrayt &json_properties, const namespacet &ns, const irep_idt &identifier, const goto_programt &goto_program)

Collects the properties in the goto program into a json_arrayt

Definition show_properties.cpp:126

show_properties.h

Show the properties.

CHECK_RETURN

#define CHECK_RETURN(CONDITION)

Definition invariant.h:495

CBMC: /home/runner/work/cbmc/cbmc/src/goto-diff/goto_diff_base.cpp Source File