CBMC
Loading...
Searching...
No Matches
source_lines.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Source Lines
4
5Author: 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
31
33{
34public:
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
62private:
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)
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.
std::map< std::string, function_linest > block_linest
A set of lines from multiple files.
std::map< std::string, linest > function_linest
A set of lines from multiple function.
source_linest()=default
Constructors.
std::set< mp_integer > linest
A set of lines from a single function.