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  forall_goto_program_instructions(it, goto_program)
36  {
37  if(it->is_backwards_goto())
38  {
39  std::cout << "Loop " << goto_programt::loop_id(function_id, *it)
40  << ":"
41  << "\n";
42 
43  std::cout << " " << it->source_location << "\n";
44  std::cout << "\n";
45  }
46  }
47  break;
48  }
50  {
51  forall_goto_program_instructions(it, goto_program)
52  {
53  if(it->is_backwards_goto())
54  {
55  std::string id = id2string(goto_programt::loop_id(function_id, *it));
56 
57  xmlt xml_loop("loop", {{"name", id}}, {});
58  xml_loop.new_element("loop-id").data=id;
59  xml_loop.new_element()=xml(it->source_location);
60  std::cout << xml_loop << "\n";
61  }
62  }
63  break;
64  }
66  UNREACHABLE; // use function below
67  }
68 }
69 
72  const irep_idt &function_id,
73  const goto_programt &goto_program,
74  json_arrayt &loops)
75 {
76  PRECONDITION(ui == ui_message_handlert::uit::JSON_UI); // use function above
77 
78  forall_goto_program_instructions(it, goto_program)
79  {
80  if(it->is_backwards_goto())
81  {
82  std::string id = id2string(goto_programt::loop_id(function_id, *it));
83 
84  loops.push_back(
85  json_objectt({{"name", json_stringt(id)},
86  {"sourceLocation", json(it->source_location)}}));
87  }
88  }
89 }
90 
93  const goto_functionst &goto_functions)
94 {
95  switch(ui)
96  {
99  for(const auto &f: goto_functions.function_map)
100  show_loop_ids(ui, f.first, f.second.body);
101  break;
102 
104  json_objectt json_result;
105  json_arrayt &loops=json_result["loops"].make_array();
106 
107  for(const auto &f : goto_functions.function_map)
108  show_loop_ids_json(ui, f.first, f.second.body, loops);
109 
110  std::cout << ",\n" << json_result;
111  break;
112  }
113 }
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:755
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:70
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
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_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:73
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
forall_goto_program_instructions
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:1196
xmlt::new_element
xmlt & new_element(const std::string &key)
Definition: xml.h:95
json_stringt
Definition: json.h:270