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 
30  const irep_idt &function_identifier,
31  const goto_programt &goto_program)
32 {
33  switch(ui)
34  {
36  {
37  forall_goto_program_instructions(it, goto_program)
38  {
39  if(it->is_backwards_goto())
40  {
41  unsigned loop_id=it->loop_number;
42 
43  std::cout << "Loop " << function_identifier << "." << loop_id << ":"
44  << "\n";
45 
46  std::cout << " " << it->source_location << "\n";
47  std::cout << "\n";
48  }
49  }
50  break;
51  }
53  {
54  forall_goto_program_instructions(it, goto_program)
55  {
56  if(it->is_backwards_goto())
57  {
58  unsigned loop_id=it->loop_number;
59  std::string id =
60  id2string(function_identifier) + "." + std::to_string(loop_id);
61 
62  xmlt xml_loop("loop");
63  xml_loop.set_attribute("name", id);
64  xml_loop.new_element("loop-id").data=id;
65  xml_loop.new_element()=xml(it->source_location);
66  std::cout << xml_loop << "\n";
67  }
68  }
69  break;
70  }
72  UNREACHABLE; // use function below
73  }
74 }
75 
78  const irep_idt &function_identifier,
79  const goto_programt &goto_program,
80  json_arrayt &loops)
81 {
82  PRECONDITION(ui == ui_message_handlert::uit::JSON_UI); // use function above
83 
84  forall_goto_program_instructions(it, goto_program)
85  {
86  if(it->is_backwards_goto())
87  {
88  unsigned loop_id=it->loop_number;
89  std::string id =
90  id2string(function_identifier) + "." + std::to_string(loop_id);
91 
92  json_objectt &loop=loops.push_back().make_object();
93  loop["name"]=json_stringt(id);
94  loop["sourceLocation"]=json(it->source_location);
95  }
96  }
97 }
98 
101  const goto_functionst &goto_functions)
102 {
103  switch(ui)
104  {
107  for(const auto &f: goto_functions.function_map)
108  show_loop_ids(ui, f.first, f.second.body);
109  break;
110 
112  json_objectt json_result;
113  json_arrayt &loops=json_result["loops"].make_array();
114 
115  for(const auto &f : goto_functions.function_map)
116  show_loop_ids_json(ui, f.first, f.second.body, loops);
117 
118  std::cout << ",\n" << json_result;
119  break;
120  }
121 }
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:44
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
function_mapt function_map
xmlt xml(const source_locationt &location)
Definition: xml_expr.cpp:26
json_arrayt & make_array()
Definition: json.h:284
jsont & push_back(const jsont &json)
Definition: json.h:163
void show_loop_ids_json(ui_message_handlert::uit ui, const irep_idt &function_identifier, const goto_programt &goto_program, json_arrayt &loops)
Definition: loop_ids.cpp:76
Expressions in JSON.
void set_attribute(const std::string &attribute, unsigned value)
Definition: xml.cpp:175
Loop IDs.
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
Definition: xml.h:18
A collection of goto functions.
std::string data
Definition: xml.h:30
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
xmlt & new_element(const std::string &key)
Definition: xml.h:86
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:478
json_objectt & make_object()
Definition: json.h:290
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:804
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
json_objectt json(const source_locationt &location)
Definition: json_expr.cpp:87