CBMC
source_location.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: 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 
19 class source_locationt:public irept
20 {
21 public:
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  {
43  return get(ID_working_directory);
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"))
64  const irep_idt &get_function() const
65  {
66  return get(ID_function);
67  }
68 
69  const irep_idt &get_property_id() const
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 
84  const irep_idt &get_case_number() const
85  {
86  return get(ID_switch_case_number);
87  }
88 
90  {
91  return get(ID_java_bytecode_index);
92  }
93 
95  {
96  return find(ID_basic_block_source_lines);
97  }
98 
99  void set_file(const irep_idt &file)
100  {
101  set(ID_file, file);
102  }
103 
105  {
106  set(ID_working_directory, cwd);
107  }
108 
109  void set_line(const irep_idt &line)
110  {
111  set(ID_line, line);
112  }
113 
114  void set_line(unsigned line)
115  {
116  set(ID_line, line);
117  }
118 
119  void set_column(const irep_idt &column)
120  {
121  set(ID_column, column);
122  }
123 
124  void set_column(unsigned column)
125  {
126  set(ID_column, column);
127  }
128 
129  DEPRECATED(SINCE(2022, 10, 13, "use identifier of containing function"))
130  void set_function(const irep_idt &function)
131  {
132  set(ID_function, function);
133  }
134 
135  void set_property_id(const irep_idt &property_id)
136  {
137  set(ID_property_id, property_id);
138  }
139 
140  void set_property_class(const irep_idt &property_class)
141  {
142  set(ID_property_class, property_class);
143  }
144 
146  {
147  set(ID_comment, comment);
148  }
149 
150  // for switch case number
151  void set_case_number(const irep_idt &number)
152  {
153  set(ID_switch_case_number, number);
154  }
155 
157  {
158  set(ID_java_bytecode_index, index);
159  }
160 
162  {
163  add(ID_basic_block_source_lines, std::move(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 
192  std::optional<std::string> full_path() const;
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 
204 protected:
205  std::string as_string(bool print_cwd) const;
206 };
207 
208 std::ostream &operator <<(std::ostream &, const source_locationt &);
209 
210 template <>
212 {
213  static std::string
214  diagnostics_as_string(const source_locationt &source_location)
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:38
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:360
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
named_subt & get_named_sub()
Definition: irep.h:446
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 merge(const source_locationt &from)
Set all unset source-location fields in this object to their values in 'from'.
const irep_idt & get_function() const
const irep_idt & get_working_directory() const
void set_column(const irep_idt &column)
void set_comment(const irep_idt &comment)
bool is_built_in() const
const irep_idt & get_column() const
void set_property_id(const irep_idt &property_id)
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_property_id() const
static const source_locationt & nil()
const irep_idt & get_java_bytecode_index() const
const irep_idt & get_comment() const
void set_property_class(const irep_idt &property_class)
const irept::named_subt & get_pragmas() const
const irep_idt & get_property_class() const
void set_case_number(const irep_idt &number)
void set_java_bytecode_index(const irep_idt &index)
const irep_idt & get_line() const
const irep_idt & get_case_number() const
const irep_idt & get_file() const
void add_pragma(const irep_idt &pragma)
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 irept & get_basic_block_source_lines() 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:40
static std::string comment(const rw_set_baset::entryt &entry, bool write)
Definition: race_check.cpp:108
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