CBMC
source_lines.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Source Lines
4 
5 Author: Mark R. Tuttle
6 
7 \*******************************************************************/
8 
11 
19 
20 #ifndef CPROVER_GOTO_INSTRUMENT_SOURCE_LINES_H
21 #define CPROVER_GOTO_INSTRUMENT_SOURCE_LINES_H
22 
23 #include <util/irep.h>
24 #include <util/mp_arith.h>
25 
26 #include <map>
27 #include <set>
28 #include <string>
29 
30 class source_locationt;
31 
33 {
34 public:
36  source_linest() = default;
37  explicit source_linest(const source_locationt &loc)
38  {
39  insert(loc);
40  }
41 
44  void insert(const source_locationt &loc);
45 
53  std::string to_string() const;
54 
60  irept to_irep() const;
61 
62 private:
64  using linest = std::set<mp_integer>;
66  using function_linest = std::map<std::string, linest>;
68  using block_linest = std::map<std::string, function_linest>;
69 
71 };
72 
73 #endif // CPROVER_GOTO_INSTRUMENT_SOURCE_LINES_H
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:364
void insert(const source_locationt &loc)
Insert a line (a source location) into the set of lines.
source_linest(const source_locationt &loc)
Definition: source_lines.h:37
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.
std::map< std::string, function_linest > block_linest
A set of lines from multiple files.
Definition: source_lines.h:68
std::map< std::string, linest > function_linest
A set of lines from multiple function.
Definition: source_lines.h:66
source_linest()=default
Constructors.
std::set< mp_integer > linest
A set of lines from a single function.
Definition: source_lines.h:64