CBMC
Loading...
Searching...
No Matches
source_lines.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Source Lines
4
5Author: Mark R. Tuttle
6
7\*******************************************************************/
8
11
12#include "source_lines.h"
13
15#include <util/range.h>
17#include <util/string_utils.h>
18
19#include <sstream>
20
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;
33
34 block_lines[file][func].insert(line);
35}
36
37std::string source_linest::to_string() const
38{
39 std::stringstream result;
40 const auto full_map =
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 + ':' +
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
59{
60 irept result;
61
62 for(const auto &file_entry : block_lines)
63 {
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());
70 }
71 result.add(file_entry.first, std::move(file_result));
72 }
73
74 return result;
75}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition irep.h:364
irept & add(const irep_idt &name)
Definition irep.cpp:103
void insert(const source_locationt &loc)
Insert a line (a source location) into the set of lines.
block_linest block_lines
irept to_irep() const
Construct an irept representing the set of lines.
std::string to_string() const
Construct a string representing the set of lines.
const irep_idt & get_function() const
const irep_idt & get_file() const
const irep_idt & get_line() const
static bool is_built_in(const std::string &s)
std::string format_number_range(const std::vector< mp_integer > &input_numbers)
create shorter representation for output
Format vector of numbers into a compressed range.
const std::string & id2string(const irep_idt &d)
Definition irep.h:44
const mp_integer string2integer(const std::string &n, unsigned base)
Definition mp_arith.cpp:54
Ranges: pair of begin and end iterators, which can be initialized from containers,...
ranget< iteratort > make_range(iteratort begin, iteratort end)
Definition range.h:522
Set of source code lines contributing to a basic block.
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.