cprover
Toggle main menu visibility
Loading...
Searching...
No Matches
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
18
#include <
goto-programs/goto_model.h
>
19
20
void
show_locations
(
21
ui_message_handlert::uit
ui,
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
{
34
case
ui_message_handlert::uit::XML_UI
:
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
52
case
ui_message_handlert::uit::PLAIN
:
53
std::cout << function_id <<
" "
<< it->location_number <<
" "
54
<< it->source_location() <<
'\n'
;
55
break
;
56
57
case
ui_message_handlert::uit::JSON_UI
:
58
UNREACHABLE
;
59
}
60
}
61
}
62
63
void
show_locations
(
64
ui_message_handlert::uit
ui,
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
}
goto_functionst::function_map
function_mapt function_map
Definition
goto_functions.h:29
goto_modelt
Definition
goto_model.h:27
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition
goto_model.h:34
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition
goto_program.h:72
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition
goto_program.h:621
source_locationt
Definition
source_location.h:20
source_locationt::get_function
const irep_idt & get_function() const
Definition
source_location.h:64
source_locationt::get_file
const irep_idt & get_file() const
Definition
source_location.h:36
source_locationt::get_line
const irep_idt & get_line() const
Definition
source_location.h:46
ui_message_handlert::uit
uit
Definition
ui_message.h:24
ui_message_handlert::uit::JSON_UI
@ JSON_UI
Definition
ui_message.h:24
ui_message_handlert::uit::XML_UI
@ XML_UI
Definition
ui_message.h:24
ui_message_handlert::uit::PLAIN
@ PLAIN
Definition
ui_message.h:24
xmlt
Definition
xml.h:21
xmlt::new_element
xmlt & new_element(const std::string &key)
Definition
xml.h:95
xmlt::data
std::string data
Definition
xml.h:39
xmlt::name
std::string name
Definition
xml.h:39
goto_model.h
Symbol Table + CFG.
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:110
show_locations
void show_locations(ui_message_handlert::uit ui, const irep_idt function_id, const goto_programt &goto_program)
Definition
show_locations.cpp:20
show_locations.h
Show program locations.
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition
invariant.h:525
irep_idt
dstringt irep_idt
Definition
verification_result.h:16
xml.h
goto-instrument
show_locations.cpp
Generated by
1.17.0