CBMC
Loading...
Searching...
No Matches
show_locations.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Show program locations
4
5Author: 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}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
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.
instructionst instructions
The list of instructions in the goto program.
const irep_idt & get_function() const
const irep_idt & get_file() const
const irep_idt & get_line() 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)
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