CBMC
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 
15 #include <util/range.h>
16 #include <util/source_location.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 
37 std::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 + ':' +
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 
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 }
bool empty() const
Definition: dstring.h:89
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:360
void set(const irep_idt &name, const irep_idt &value)
Definition: irep.h:408
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
Definition: source_lines.h:70
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_line() const
const irep_idt & get_file() 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:40
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
BigInt mp_integer
Definition: smt_terms.h:17
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.
Definition: string_utils.h:61