cprover
show_locations.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Show program locations
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "show_locations.h"
13 
14 #include <iostream>
15 
16 #include <util/xml.h>
17 #include <util/xml_irep.h>
18 
19 #include <langapi/language_util.h>
20 
22 
25  const irep_idt function_id,
26  const goto_programt &goto_program)
27 {
28  for(goto_programt::instructionst::const_iterator
29  it=goto_program.instructions.begin();
30  it!=goto_program.instructions.end();
31  it++)
32  {
33  const source_locationt &source_location=it->source_location;
34 
35  switch(ui)
36  {
38  {
39  xmlt xml("program_location");
40  xml.new_element("function").data=id2string(function_id);
41  xml.new_element("id").data=std::to_string(it->location_number);
42 
43  xmlt &l=xml.new_element();
44  l.name="location";
45 
46  l.new_element("line").data=id2string(source_location.get_line());
47  l.new_element("file").data=id2string(source_location.get_file());
48  l.new_element("function").data=
49  id2string(source_location.get_function());
50 
51  std::cout << xml << '\n';
52  }
53  break;
54 
56  std::cout << function_id << " "
57  << it->location_number << " "
58  << it->source_location << '\n';
59  break;
60 
63  }
64  }
65 }
66 
69  const goto_modelt &goto_model)
70 {
71  for(const auto &f : goto_model.goto_functions.function_map)
72  show_locations(ui, f.first, f.second.body);
73 }
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
source_locationt::get_function
const irep_idt & get_function() const
Definition: source_location.h:56
ui_message_handlert::uit::XML_UI
@ XML_UI
goto_model.h
Symbol Table + CFG.
xml_irep.h
goto_modelt
Definition: goto_model.h:26
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:55
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:27
xml.h
source_locationt::get_line
const irep_idt & get_line() const
Definition: source_location.h:46
ui_message_handlert::uit
uit
Definition: ui_message.h:22
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
language_util.h
xmlt::name
std::string name
Definition: xml.h:39
xmlt
Definition: xml.h:21
source_locationt
Definition: source_location.h:20
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:585
show_locations.h
Show program locations.
show_locations
void show_locations(ui_message_handlert::uit ui, const irep_idt function_id, const goto_programt &goto_program)
Definition: show_locations.cpp: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
source_locationt::get_file
const irep_idt & get_file() const
Definition: source_location.h:36
xmlt::data
std::string data
Definition: xml.h:39
xmlt::new_element
xmlt & new_element(const std::string &key)
Definition: xml.h:95