cprover
Loading...
Searching...
No Matches
source_location.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9
10#ifndef CPROVER_UTIL_SOURCE_LOCATION_H
11#define CPROVER_UTIL_SOURCE_LOCATION_H
12
13#include "irep.h"
14#include "optional.h"
15
16#include <string>
17
19{
20public:
22 {
23 }
24
25 std::string as_string() const
26 {
27 return as_string(false);
28 }
29
30 std::string as_string_with_cwd() const
31 {
32 return as_string(true);
33 }
34
35 const irep_idt &get_file() const
36 {
37 return get(ID_file);
38 }
39
41 {
42 return get(ID_working_directory);
43 }
44
45 const irep_idt &get_line() const
46 {
47 return get(ID_line);
48 }
49
50 const irep_idt &get_column() const
51 {
52 return get(ID_column);
53 }
54
55 const irep_idt &get_function() const
56 {
57 return get(ID_function);
58 }
59
61 {
62 return get(ID_property_id);
63 }
64
66 {
67 return get(ID_property_class);
68 }
69
70 const irep_idt &get_comment() const
71 {
72 return get(ID_comment);
73 }
74
76 {
77 return get(ID_switch_case_number);
78 }
79
81 {
82 return get(ID_java_bytecode_index);
83 }
84
86 {
87 return get(ID_basic_block_covered_lines);
88 }
89
91 {
92 return get(ID_basic_block_source_lines);
93 }
94
95 void set_file(const irep_idt &file)
96 {
97 set(ID_file, file);
98 }
99
101 {
102 set(ID_working_directory, cwd);
103 }
104
105 void set_line(const irep_idt &line)
106 {
107 set(ID_line, line);
108 }
109
110 void set_line(unsigned line)
111 {
112 set(ID_line, line);
113 }
114
115 void set_column(const irep_idt &column)
116 {
117 set(ID_column, column);
118 }
119
120 void set_column(unsigned column)
121 {
122 set(ID_column, column);
123 }
124
125 void set_function(const irep_idt &function)
126 {
127 set(ID_function, function);
128 }
129
130 void set_property_id(const irep_idt &property_id)
131 {
132 set(ID_property_id, property_id);
133 }
134
135 void set_property_class(const irep_idt &property_class)
136 {
137 set(ID_property_class, property_class);
138 }
139
141 {
142 set(ID_comment, comment);
143 }
144
145 // for switch case number
146 void set_case_number(const irep_idt &number)
147 {
148 set(ID_switch_case_number, number);
149 }
150
152 {
153 set(ID_java_bytecode_index, index);
154 }
155
156 void set_basic_block_covered_lines(const irep_idt &covered_lines)
157 {
158 return set(ID_basic_block_covered_lines, covered_lines);
159 }
160
161 void set_basic_block_source_lines(const irep_idt &source_lines)
162 {
163 return set(ID_basic_block_source_lines, source_lines);
164 }
165
166 void set_hide()
167 {
168 set(ID_hide, true);
169 }
170
171 bool get_hide() const
172 {
173 return get_bool(ID_hide);
174 }
175
176 static bool is_built_in(const std::string &s);
177
178 bool is_built_in() const
179 {
180 return is_built_in(id2string(get_file()));
181 }
182
185 void merge(const source_locationt &from);
186
187 static const source_locationt &nil()
188 {
189 return static_cast<const source_locationt &>(get_nil_irep());
190 }
191
193
194 void add_pragma(const irep_idt &pragma)
195 {
196 add(ID_pragma).add(pragma);
197 }
198
200 {
201 return find(ID_pragma).get_named_sub();
202 }
203
204protected:
205 std::string as_string(bool print_cwd) const;
206};
207
208std::ostream &operator <<(std::ostream &, const source_locationt &);
209
210template <>
212{
213 static std::string
215 {
216 return "source location: " + source_location.as_string();
217 }
218};
219
220#endif // CPROVER_UTIL_SOURCE_LOCATION_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:372
bool get_bool(const irep_idt &name) const
Definition: irep.cpp:58
const irept & find(const irep_idt &name) const
Definition: irep.cpp:106
const irep_idt & get(const irep_idt &name) const
Definition: irep.cpp:45
void set(const irep_idt &name, const irep_idt &value)
Definition: irep.h:420
irept & add(const irep_idt &name)
Definition: irep.cpp:116
named_subt & get_named_sub()
Definition: irep.h:458
void merge(const source_locationt &from)
Set all unset source-location fields in this object to their values in 'from'.
void set_column(const irep_idt &column)
optionalt< std::string > full_path() const
Get a path to the file, including working directory.
void set_comment(const irep_idt &comment)
bool is_built_in() const
const irep_idt & get_basic_block_covered_lines() const
void set_property_id(const irep_idt &property_id)
void set_basic_block_covered_lines(const irep_idt &covered_lines)
static const source_locationt & nil()
const irep_idt & get_property_id() const
void set_line(unsigned line)
void set_working_directory(const irep_idt &cwd)
const irep_idt & get_java_bytecode_index() const
const irep_idt & get_column() const
const irep_idt & get_case_number() const
void set_property_class(const irep_idt &property_class)
const irep_idt & get_function() const
const irep_idt & get_working_directory() const
const irep_idt & get_file() const
void set_case_number(const irep_idt &number)
void set_java_bytecode_index(const irep_idt &index)
const irep_idt & get_line() const
void add_pragma(const irep_idt &pragma)
const irep_idt & get_property_class() const
const irept::named_subt & get_pragmas() const
bool get_hide() const
std::string as_string() const
std::string as_string_with_cwd() const
void set_basic_block_source_lines(const irep_idt &source_lines)
void set_column(unsigned column)
void set_file(const irep_idt &file)
void set_line(const irep_idt &line)
const irep_idt & get_basic_block_source_lines() const
const irep_idt & get_comment() const
void set_function(const irep_idt &function)
const irept & get_nil_irep()
Definition: irep.cpp:20
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
nonstd::optional< T > optionalt
Definition: optional.h:35
static std::string comment(const rw_set_baset::entryt &entry, bool write)
Definition: race_check.cpp:109
std::ostream & operator<<(std::ostream &, const source_locationt &)
static std::string diagnostics_as_string(const source_locationt &source_location)
Helper to give us some diagnostic in a usable form on assertion failure.
Definition: invariant.h:299
Definition: kdev_t.h:19