cprover
loop_ids.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Loop IDs
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "loop_ids.h"
13 
14 #include <iostream>
15 
16 #include <util/json_irep.h>
17 #include <util/xml_irep.h>
18 
21  const goto_modelt &goto_model)
22 {
23  show_loop_ids(ui, goto_model.goto_functions);
24 }
25 
28  const irep_idt &function_id,
29  const goto_programt &goto_program)
30 {
31  switch(ui)
32  {
34  {
35  for(const auto &instruction : goto_program.instructions)
36  {
37  if(instruction.is_backwards_goto())
38  {
39  std::cout << "Loop "
40  << goto_programt::loop_id(function_id, instruction) << ":"
41  << "\n";
42 
43  std::cout << " " << instruction.source_location << "\n";
44  std::cout << "\n";
45  }
46  }
47  break;
48  }
50  {
51  for(const auto &instruction : goto_program.instructions)
52  {
53  if(instruction.is_backwards_goto())
54  {
55  std::string id =
56  id2string(goto_programt::loop_id(function_id, instruction));
57 
58  xmlt xml_loop("loop", {{"name", id}}, {});
59  xml_loop.new_element("loop-id").data=id;
60  xml_loop.new_element() = xml(instruction.source_location);
61  std::cout << xml_loop << "\n";
62  }
63  }
64  break;
65  }
67  UNREACHABLE; // use function below
68  }
69 }
70 
73  const irep_idt &function_id,
74  const goto_programt &goto_program,
75  json_arrayt &loops)
76 {
77  PRECONDITION(ui == ui_message_handlert::uit::JSON_UI); // use function above
78 
79  for(const auto &instruction : goto_program.instructions)
80  {
81  if(instruction.is_backwards_goto())
82  {
83  std::string id =
84  id2string(goto_programt::loop_id(function_id, instruction));
85 
86  loops.push_back(
87  json_objectt({{"name", json_stringt(id)},
88  {"sourceLocation", json(instruction.source_location)}}));
89  }
90  }
91 }
92 
95  const goto_functionst &goto_functions)
96 {
97  switch(ui)
98  {
101  for(const auto &f: goto_functions.function_map)
102  show_loop_ids(ui, f.first, f.second.body);
103  break;
104 
106  json_objectt json_result;
107  json_arrayt &loops=json_result["loops"].make_array();
108 
109  for(const auto &f : goto_functions.function_map)
110  show_loop_ids_json(ui, f.first, f.second.body, loops);
111 
112  std::cout << ",\n" << json_result;
113  break;
114  }
115 }
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
ui_message_handlert::uit::XML_UI
@ XML_UI
xml_irep.h
goto_modelt
Definition: goto_model.h:26
show_loop_ids
void show_loop_ids(ui_message_handlert::uit ui, const goto_modelt &goto_model)
Definition: loop_ids.cpp:19
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:27
json_irep.h
Util.
json_arrayt
Definition: json.h:165
json_objectt
Definition: json.h:300
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:739
ui_message_handlert::uit
uit
Definition: ui_message.h:22
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:71
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
xml
xmlt xml(const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:105
ui_message_handlert::uit::JSON_UI
@ JSON_UI
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
json
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:114
jsont::make_array
json_arrayt & make_array()
Definition: json.h:420
xmlt
Definition: xml.h:21
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:569
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
ui_message_handlert::uit::PLAIN
@ PLAIN
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:74
loop_ids.h
Loop IDs.
xmlt::data
std::string data
Definition: xml.h:39
json_arrayt::push_back
jsont & push_back(const jsont &json)
Definition: json.h:212
xmlt::new_element
xmlt & new_element(const std::string &key)
Definition: xml.h:95
json_stringt
Definition: json.h:270