CBMC
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 
19 
22  const irep_idt function_id,
23  const goto_programt &goto_program)
24 {
25  for(goto_programt::instructionst::const_iterator
26  it=goto_program.instructions.begin();
27  it!=goto_program.instructions.end();
28  it++)
29  {
30  const source_locationt &source_location = it->source_location();
31 
32  switch(ui)
33  {
35  {
36  xmlt xml("program_location");
37  xml.new_element("function").data=id2string(function_id);
38  xml.new_element("id").data=std::to_string(it->location_number);
39 
40  xmlt &l=xml.new_element();
41  l.name="location";
42 
43  l.new_element("line").data=id2string(source_location.get_line());
44  l.new_element("file").data=id2string(source_location.get_file());
45  l.new_element("function").data=
46  id2string(source_location.get_function());
47 
48  std::cout << xml << '\n';
49  }
50  break;
51 
53  std::cout << function_id << " " << it->location_number << " "
54  << it->source_location() << '\n';
55  break;
56 
59  }
60  }
61 }
62 
65  const goto_modelt &goto_model)
66 {
67  for(const auto &f : goto_model.goto_functions.function_map)
68  show_locations(ui, f.first, f.second.body);
69 }
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
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
const irep_idt & get_function() const
const irep_idt & get_line() const
const irep_idt & get_file() const
Definition: xml.h:21
xmlt & new_element(const std::string &key)
Definition: xml.h:95
std::string data
Definition: xml.h:39
std::string name
Definition: xml.h:39
Symbol Table + CFG.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
xmlt xml(const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:110
void show_locations(ui_message_handlert::uit ui, const irep_idt function_id, const goto_programt &goto_program)
Show program locations.
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:525
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.