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 }
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
A collection of goto functions.
function_mapt function_map
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:74
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:556
static irep_idt loop_id(const irep_idt &function_id, const instructiont &instruction)
Human-readable loop name.
Definition: goto_program.h:726
jsont & push_back(const jsont &json)
Definition: json.h:212
json_arrayt & make_array()
Definition: json.h:420
Definition: xml.h:21
xmlt & new_element(const std::string &key)
Definition: xml.h:95
std::string data
Definition: xml.h:39
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
void show_loop_ids(ui_message_handlert::uit ui, const goto_modelt &goto_model)
Definition: loop_ids.cpp:19
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
Loop IDs.
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:114
xmlt xml(const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:105
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
#define PRECONDITION(CONDITION)
Definition: invariant.h:464