cprover
Toggle main menu visibility
Loading...
Searching...
No Matches
source_lines.cpp
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module: Source Lines
4
5
Author: Mark R. Tuttle
6
7
\*******************************************************************/
8
11
12
#include "
source_lines.h
"
13
14
#include <
util/format_number_range.h
>
15
#include <
util/range.h
>
16
#include <
util/source_location.h
>
17
#include <
util/string_utils.h
>
18
19
#include <sstream>
20
21
void
source_linest::insert
(
const
source_locationt
&loc)
22
{
23
if
(loc.
get_file
().
empty
() || loc.
is_built_in
())
24
return
;
25
const
std::string &
file
=
id2string
(loc.
get_file
());
26
27
// the function of a source location can fail to be set
28
const
std::string &func =
id2string
(loc.
get_function
());
29
30
if
(loc.
get_line
().
empty
())
31
return
;
32
mp_integer
line =
string2integer
(
id2string
(loc.
get_line
()));
33
34
block_lines
[
file
][func].insert(line);
35
}
36
37
std::string
source_linest::to_string
()
const
38
{
39
std::stringstream result;
40
const
auto
full_map =
41
make_range
(
block_lines
)
42
.map([&](
const
block_linest::value_type &file_entry) {
43
std::stringstream ss;
44
const
auto
map =
make_range
(file_entry.second)
45
.map([&](
const
function_linest::value_type &pair) {
46
std::vector<mp_integer> line_numbers(
47
pair.second.begin(), pair.second.end());
48
return
file_entry.first +
':'
+ pair.first +
':'
+
49
format_number_range
(line_numbers);
50
});
51
join_strings
(ss, map.begin(), map.end(),
"; "
);
52
return
ss.str();
53
});
54
join_strings
(result, full_map.begin(), full_map.end(),
"; "
);
55
return
result.str();
56
}
57
58
irept
source_linest::to_irep
()
const
59
{
60
irept
result;
61
62
for
(
const
auto
&file_entry :
block_lines
)
63
{
64
irept
file_result;
65
for
(
const
auto
&lines_entry : file_entry.second)
66
{
67
std::vector<mp_integer> line_numbers(
68
lines_entry.second.begin(), lines_entry.second.end());
69
file_result.
set
(lines_entry.first,
format_number_range
(line_numbers));
70
}
71
result.
add
(file_entry.first, std::move(file_result));
72
}
73
74
return
result;
75
}
dstringt::empty
bool empty() const
Definition
dstring.h:89
irept
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition
irep.h:364
irept::set
void set(const irep_idt &name, const irep_idt &value)
Definition
irep.h:412
irept::add
irept & add(const irep_idt &name)
Definition
irep.cpp:103
source_linest::insert
void insert(const source_locationt &loc)
Insert a line (a source location) into the set of lines.
Definition
source_lines.cpp:21
source_linest::block_lines
block_linest block_lines
Definition
source_lines.h:70
source_linest::to_irep
irept to_irep() const
Construct an irept representing the set of lines.
Definition
source_lines.cpp:58
source_linest::to_string
std::string to_string() const
Construct a string representing the set of lines.
Definition
source_lines.cpp:37
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
source_locationt::is_built_in
static bool is_built_in(const std::string &s)
Definition
source_location.cpp:16
format_number_range
std::string format_number_range(const std::vector< mp_integer > &input_numbers)
create shorter representation for output
Definition
format_number_range.cpp:24
format_number_range.h
Format vector of numbers into a compressed range.
id2string
const std::string & id2string(const irep_idt &d)
Definition
irep.h:44
string2integer
const mp_integer string2integer(const std::string &n, unsigned base)
Definition
mp_arith.cpp:54
range.h
Ranges: pair of begin and end iterators, which can be initialized from containers,...
make_range
ranget< iteratort > make_range(iteratort begin, iteratort end)
Definition
range.h:522
mp_integer
BigInt mp_integer
Definition
smt_terms.h:17
source_lines.h
Set of source code lines contributing to a basic block.
source_location.h
string_utils.h
join_strings
Stream & join_strings(Stream &&os, const It b, const It e, const Delimiter &delimiter, TransformFunc &&transform_func)
Prints items to an stream, separated by a constant delimiter.
Definition
string_utils.h:61
file
Definition
kdev_t.h:19
goto-instrument
source_lines.cpp
Generated by
1.17.0