CBMC: /home/runner/work/cbmc/cbmc/src/goto-programs/loop_ids.cpp Source File

21 void show_loop_ids(

22 ui_message_handlert::uit ui,

23 const goto_modelt &goto_model)

24{

25 show_loop_ids(ui, goto_model.goto_functions);

26}

28 void show_loop_ids(

29 ui_message_handlert::uit ui,

30 const irep_idt &function_id,

31 const goto_programt &goto_program)

32{

33 switch(ui)

34 {

35 case ui_message_handlert::uit::PLAIN:

36 {

37 for(const auto &instruction : goto_program.instructions)

38 {

39 if(instruction.is_backwards_goto())

40 {

41 std::cout << "Loop "

42 << goto_programt::loop_id(function_id, instruction) << ":"

43 << "\n";

44

45 std::cout << " " << instruction.source_location() << "\n";

46 std::cout << "\n";

47 }

48 }

49 break;

50 }

51 case ui_message_handlert::uit::XML_UI:

52 {

53 for(const auto &instruction : goto_program.instructions)

54 {

55 if(instruction.is_backwards_goto())

56 {

57 std::string id =

58 id2string(goto_programt::loop_id(function_id, instruction));

59

60 xmlt xml_loop("loop", {{"name", id}}, {});

61 xml_loop.new_element("loop-id").data=id;

62 xml_loop.new_element() = xml(instruction.source_location());

63 std::cout << xml_loop << "\n";

64 }

65 }

66 break;

67 }

68 case ui_message_handlert::uit::JSON_UI:

69 UNREACHABLE; // use function below

70 }

71}

73 void show_loop_ids_json(

74 ui_message_handlert::uit ui,

75 const irep_idt &function_id,

76 const goto_programt &goto_program,

77 json_arrayt &loops)

78{

79 PRECONDITION(ui == ui_message_handlert::uit::JSON_UI); // use function above

80

81 for(const auto &instruction : goto_program.instructions)

82 {

83 if(instruction.is_backwards_goto())

84 {

85 std::string id =

86 id2string(goto_programt::loop_id(function_id, instruction));

87

88 loops.push_back(json_objectt(

89 {{"name", json_stringt(id)},

90 {"sourceLocation", json(instruction.source_location())}}));

91 }

92 }

93}

95 void show_loop_ids(

96 ui_message_handlert::uit ui,

97 const goto_functionst &goto_functions)

98{

99 switch(ui)

100 {

101 case ui_message_handlert::uit::PLAIN:

102 case ui_message_handlert::uit::XML_UI:

103 for(const auto &f: goto_functions.function_map)

104 show_loop_ids(ui, f.first, f.second.body);

105 break;

106

107 case ui_message_handlert::uit::JSON_UI:

108 {

109 json_objectt json_result;

110 json_arrayt &loops=json_result["loops"].make_array();

111

112 for(const auto &f : goto_functions.function_map)

113 show_loop_ids_json(ui, f.first, f.second.body, loops);

114

115 std::cout << ",\n" << json_result;

116 break;

117 }

118 }

119}

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_functionst

A collection of goto functions.

Definition goto_functions.h:25

goto_functionst::function_map

function_mapt function_map

Definition goto_functions.h:29

goto_modelt

Definition goto_model.h:27

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

goto_programt::loop_id

static irep_idt loop_id(const irep_idt &function_id, const instructiont &instruction)

Human-readable loop name.

Definition goto_program.h:791

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

ui_message_handlert::uit

uit

Definition ui_message.h:24

ui_message_handlert::uit::JSON_UI

@ JSON_UI

ui_message_handlert::uit::XML_UI

@ XML_UI

ui_message_handlert::uit::PLAIN

@ PLAIN

xmlt

Definition xml.h:21

goto_model.h

Symbol Table + CFG.

id2string

const std::string & id2string(const irep_idt &d)

Definition irep.h:44

json_irep.h

Util.

show_loop_ids

void show_loop_ids(ui_message_handlert::uit ui, const goto_modelt &goto_model)

Definition loop_ids.cpp:21

show_loop_ids_json

void show_loop_ids_json(ui_message_handlert::uit ui, const irep_idt &function_id, const goto_programt &goto_program, json_arrayt &loops)

Definition loop_ids.cpp:73

loop_ids.h

Loop IDs.

json

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

Definition properties.cpp:120

xml

xmlt xml(const irep_idt &property_id, const property_infot &property_info)

Definition properties.cpp:110

UNREACHABLE

#define UNREACHABLE

This should be used to mark dead code.

Definition invariant.h:525

PRECONDITION

#define PRECONDITION(CONDITION)

Definition invariant.h:463

xml_irep.h