CBMC
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 "deprecate.h"
14#include "irep.h"
15
16#include <optional>
17#include <string>
18
20{
21public:
23 {
24 }
25
26 std::string as_string() const
27 {
28 return as_string(false);
29 }
30
31 std::string as_string_with_cwd() const
32 {
33 return as_string(true);
34 }
35
36 const irep_idt &get_file() const
37 {
38 return get(ID_file);
39 }
40
42 {
44 }
45
46 const irep_idt &get_line() const
47 {
48 return get(ID_line);
49 }
50
51 const irep_idt &get_column() const
52 {
53 return get(ID_column);
54 }
55
56 // This method is problematic for the following reasons:
57 // 1) There is ambiguity whether
58 // the returned string is an identifier or human-readable.
59 // 2) Furthermore, the linker renames functions, and is unable
60 // to adjust all source locations.
61 // 3) The name of the function is not strictly a source location.
62 // It will be removed.
63 DEPRECATED(SINCE(2022, 10, 13, "use identifier of containing function"))
65 {
66 return get(ID_function);
67 }
68
70 {
71 return get(ID_property_id);
72 }
73
75 {
76 return get(ID_property_class);
77 }
78
79 const irep_idt &get_comment() const
80 {
81 return get(ID_comment);
82 }
83
85 {
87 }
88
90 {
92 }
93
98
99 bool property_fatal() const
100 {
102 }
103
104 void set_file(const irep_idt &file)
105 {
106 set(ID_file, file);
107 }
108
113
114 void set_line(const irep_idt &line)
115 {
116 set(ID_line, line);
117 }
118
119 void set_line(unsigned line)
120 {
121 set(ID_line, line);
122 }
123
124 void set_column(const irep_idt &column)
125 {
126 set(ID_column, column);
127 }
128
129 void set_column(unsigned column)
130 {
131 set(ID_column, column);
132 }
133
134 DEPRECATED(SINCE(2022, 10, 13, "use identifier of containing function"))
136 {
137 set(ID_function, function);
138 }
139
140 void set_property_id(const irep_idt &property_id)
141 {
142 set(ID_property_id, property_id);
143 }
144
145 void set_property_class(const irep_idt &property_class)
146 {
147 set(ID_property_class, property_class);
148 }
149
151 {
153 }
154
155 // for switch case number
156 void set_case_number(const irep_idt &number)
157 {
158 set(ID_switch_case_number, number);
159 }
160
162 {
164 }
165
167 {
168 add(ID_basic_block_source_lines, std::move(source_lines));
169 }
170
172 {
174 set(ID_property_fatal, true);
175 else
177 }
178
179 void set_hide()
180 {
181 set(ID_hide, true);
182 }
183
184 bool get_hide() const
185 {
186 return get_bool(ID_hide);
187 }
188
189 static bool is_built_in(const std::string &s);
190
191 bool is_built_in() const
192 {
193 return is_built_in(id2string(get_file()));
194 }
195
198 void merge(const source_locationt &from);
199
200 static const source_locationt &nil()
201 {
202 return static_cast<const source_locationt &>(get_nil_irep());
203 }
204
205 std::optional<std::string> full_path() const;
206
208 {
210 }
211
213 {
214 return find(ID_pragma).get_named_sub();
215 }
216
217protected:
218 std::string as_string(bool print_cwd) const;
219};
220
221std::ostream &operator <<(std::ostream &, const source_locationt &);
222
223template <>
225{
226 static std::string
228 {
229 return "source location: " + source_location.as_string();
230 }
231};
232
233#endif // CPROVER_UTIL_SOURCE_LOCATION_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition irep.h:364
bool get_bool(const irep_idt &name) const
Definition irep.cpp:57
const irept & find(const irep_idt &name) const
Definition irep.cpp:93
const irep_idt & get(const irep_idt &name) const
Definition irep.cpp:44
void remove(const irep_idt &name)
Definition irep.cpp:87
void set(const irep_idt &name, const irep_idt &value)
Definition irep.h:412
irept & add(const irep_idt &name)
Definition irep.cpp:103
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)
void property_fatal(bool _property_fatal)
void set_comment(const irep_idt &comment)
bool is_built_in() const
void set_property_id(const irep_idt &property_id)
static const source_locationt & nil()
bool property_fatal() const
const irep_idt & get_property_id() const
void set_basic_block_source_lines(irept source_lines)
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)
const irept & get_basic_block_source_lines() const
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_column(unsigned column)
void set_file(const irep_idt &file)
void set_line(const irep_idt &line)
std::optional< std::string > full_path() const
Get a path to the file, including working directory.
const irep_idt & get_comment() const
void set_function(const irep_idt &function)
#define SINCE(year, month, day, msg)
Definition deprecate.h:26
#define DEPRECATED(msg)
Definition deprecate.h:23
const irept & get_nil_irep()
Definition irep.cpp:19
const std::string & id2string(const irep_idt &d)
Definition irep.h:44
static std::string comment(const rw_set_baset::entryt &entry, bool write)
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