CBMC
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 
19 #include "goto_model.h"
20 
23  const goto_modelt &goto_model)
24 {
25  show_loop_ids(ui, goto_model.goto_functions);
26 }
27 
30  const irep_idt &function_id,
31  const goto_programt &goto_program)
32 {
33  switch(ui)
34  {
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  }
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  }
69  UNREACHABLE; // use function below
70  }
71 }
72 
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 }
94 
97  const goto_functionst &goto_functions)
98 {
99  switch(ui)
100  {
103  for(const auto &f: goto_functions.function_map)
104  show_loop_ids(ui, f.first, f.second.body);
105  break;
106 
108  json_objectt json_result;
109  json_arrayt &loops=json_result["loops"].make_array();
110 
111  for(const auto &f : goto_functions.function_map)
112  show_loop_ids_json(ui, f.first, f.second.body, loops);
113 
114  std::cout << ",\n" << json_result;
115  break;
116  }
117 }
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
A collection of goto functions.
function_mapt function_map
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:34
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:622
static irep_idt loop_id(const irep_idt &function_id, const instructiont &instruction)
Human-readable loop name.
Definition: goto_program.h:792
jsont & push_back(const jsont &json)
Definition: json.h:212
json_arrayt & make_array()
Definition: json.h:418
Definition: xml.h:21
xmlt & new_element(const std::string &key)
Definition: xml.h:95
std::string data
Definition: xml.h:39
Symbol Table + CFG.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
void show_loop_ids(ui_message_handlert::uit ui, const goto_modelt &goto_model)
Definition: loop_ids.cpp:21
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.
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:120
xmlt xml(const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:110
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:525
#define PRECONDITION(CONDITION)
Definition: invariant.h:463