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/xml.h>
17 #include <util/xml_expr.h>
18 #include <util/json.h>
19 #include <util/json_expr.h>
20 
23  const goto_modelt &goto_model)
24 {
25  show_loop_ids(ui, goto_model.goto_functions);
26 }
27 
31 {
32  switch(ui)
33  {
35  {
37  {
38  if(it->is_backwards_goto())
39  {
40  unsigned loop_id=it->loop_number;
41 
42  std::cout << "Loop "
43  << it->function << "." << loop_id << ":" << "\n";
44 
45  std::cout << " " << it->source_location << "\n";
46  std::cout << "\n";
47  }
48  }
49  break;
50  }
52  {
54  {
55  if(it->is_backwards_goto())
56  {
57  unsigned loop_id=it->loop_number;
58  std::string id=id2string(it->function)+"."+std::to_string(loop_id);
59 
60  xmlt xml_loop("loop");
61  xml_loop.set_attribute("name", id);
62  xml_loop.new_element("loop-id").data=id;
63  xml_loop.new_element()=xml(it->source_location);
64  std::cout << xml_loop << "\n";
65  }
66  }
67  break;
68  }
70  UNREACHABLE; // use function below
71  }
72 }
73 
77  json_arrayt &loops)
78 {
79  assert(ui==ui_message_handlert::uit::JSON_UI); // use function above
80 
82  {
83  if(it->is_backwards_goto())
84  {
85  unsigned loop_id=it->loop_number;
86  std::string id=id2string(it->function)+"."+std::to_string(loop_id);
87 
88  json_objectt &loop=loops.push_back().make_object();
89  loop["name"]=json_stringt(id);
90  loop["sourceLocation"]=json(it->source_location);
91  }
92  }
93 }
94 
97  const goto_functionst &goto_functions)
98 {
99  switch(ui)
100  {
103  forall_goto_functions(it, goto_functions)
104  show_loop_ids(ui, it->second.body);
105  break;
107  json_objectt json_result;
108  json_arrayt &loops=json_result["loops"].make_array();
109 
110  forall_goto_functions(it, goto_functions)
111  show_loop_ids_json(ui, it->second.body, loops);
112 
113  std::cout << ",\n" << json_result;
114  break;
115  }
116 }
void show_loop_ids(ui_message_handlert::uit ui, const goto_modelt &goto_model)
Definition: loop_ids.cpp:21
const std::string & id2string(const irep_idt &d)
Definition: irep.h:43
xmlt xml(const source_locationt &location)
Definition: xml_expr.cpp:25
json_arrayt & make_array()
Definition: json.h:284
jsont & push_back(const jsont &json)
Definition: json.h:163
Expressions in JSON.
void set_attribute(const std::string &attribute, unsigned value)
Definition: xml.cpp:174
Loop IDs.
Definition: xml.h:18
std::string data
Definition: xml.h:30
xmlt & new_element(const std::string &name)
Definition: xml.h:86
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:70
void show_loop_ids_json(ui_message_handlert::uit ui, const goto_programt &goto_program, json_arrayt &loops)
Definition: loop_ids.cpp:74
std::string to_string(const string_constraintt &expr)
Used for debug printing.
#define UNREACHABLE
Definition: invariant.h:250
goto_programt & goto_program
Definition: cover.cpp:63
json_objectt & make_object()
Definition: json.h:290
#define forall_goto_functions(it, functions)
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:735
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
json_objectt json(const source_locationt &location)
Definition: json_expr.cpp:83