cprover
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 "invariant.h"
14 #include "irep.h"
15 #include "optional.h"
16 #include "prefix.h"
17 
18 #include <string>
19 
20 class source_locationt:public irept
21 {
22 public:
24  {
25  }
26 
27  std::string as_string() const
28  {
29  return as_string(false);
30  }
31 
32  std::string as_string_with_cwd() const
33  {
34  return as_string(true);
35  }
36 
37  const irep_idt &get_file() const
38  {
39  return get(ID_file);
40  }
41 
43  {
44  return get(ID_working_directory);
45  }
46 
47  const irep_idt &get_line() const
48  {
49  return get(ID_line);
50  }
51 
52  const irep_idt &get_column() const
53  {
54  return get(ID_column);
55  }
56 
57  const irep_idt &get_function() const
58  {
59  return get(ID_function);
60  }
61 
62  const irep_idt &get_property_id() const
63  {
64  return get(ID_property_id);
65  }
66 
68  {
69  return get(ID_property_class);
70  }
71 
72  const irep_idt &get_comment() const
73  {
74  return get(ID_comment);
75  }
76 
77  const irep_idt &get_case_number() const
78  {
79  return get(ID_switch_case_number);
80  }
81 
83  {
84  return get(ID_java_bytecode_index);
85  }
86 
88  {
89  return get(ID_basic_block_covered_lines);
90  }
91 
92  void set_file(const irep_idt &file)
93  {
94  set(ID_file, file);
95  }
96 
98  {
99  set(ID_working_directory, cwd);
100  }
101 
102  void set_line(const irep_idt &line)
103  {
104  set(ID_line, line);
105  }
106 
107  void set_line(unsigned line)
108  {
109  set(ID_line, line);
110  }
111 
112  void set_column(const irep_idt &column)
113  {
114  set(ID_column, column);
115  }
116 
117  void set_column(unsigned column)
118  {
119  set(ID_column, column);
120  }
121 
122  void set_function(const irep_idt &function)
123  {
124  set(ID_function, function);
125  }
126 
127  void set_property_id(const irep_idt &property_id)
128  {
129  set(ID_property_id, property_id);
130  }
131 
132  void set_property_class(const irep_idt &property_class)
133  {
134  set(ID_property_class, property_class);
135  }
136 
138  {
139  set(ID_comment, comment);
140  }
141 
142  // for switch case number
143  void set_case_number(const irep_idt &number)
144  {
145  set(ID_switch_case_number, number);
146  }
147 
149  {
150  set(ID_java_bytecode_index, index);
151  }
152 
153  void set_basic_block_covered_lines(const irep_idt &covered_lines)
154  {
155  return set(ID_basic_block_covered_lines, covered_lines);
156  }
157 
158  void set_hide()
159  {
160  set(ID_hide, true);
161  }
162 
163  bool get_hide() const
164  {
165  return get_bool(ID_hide);
166  }
167 
168  static bool is_built_in(const std::string &s)
169  {
170  std::string built_in1="<built-in-"; // "<built-in-additions>";
171  std::string built_in2="<builtin-"; // "<builtin-architecture-strings>";
172  return has_prefix(s, built_in1) || has_prefix(s, built_in2);
173  }
174 
175  bool is_built_in() const
176  {
177  return is_built_in(id2string(get_file()));
178  }
179 
182  void merge(const source_locationt &from);
183 
184  static const source_locationt &nil()
185  {
186  return static_cast<const source_locationt &>(get_nil_irep());
187  }
188 
190 
191 protected:
192  std::string as_string(bool print_cwd) const;
193 };
194 
195 std::ostream &operator <<(std::ostream &, const source_locationt &);
196 
197 template <>
199 {
200  static std::string
201  diagnostics_as_string(const source_locationt &source_location)
202  {
203  return "source location: " + source_location.as_string();
204  }
205 };
206 
207 #endif // CPROVER_UTIL_SOURCE_LOCATION_H
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
source_locationt::get_function
const irep_idt & get_function() const
Definition: source_location.h:57
source_locationt::get_comment
const irep_idt & get_comment() const
Definition: source_location.h:72
source_locationt::get_property_id
const irep_idt & get_property_id() const
Definition: source_location.h:62
source_locationt::get_property_class
const irep_idt & get_property_class() const
Definition: source_location.h:67
source_locationt::as_string
std::string as_string() const
Definition: source_location.h:27
source_locationt::set_comment
void set_comment(const irep_idt &comment)
Definition: source_location.h:137
source_locationt::set_function
void set_function(const irep_idt &function)
Definition: source_location.h:122
comment
std::string comment(const rw_set_baset::entryt &entry, bool write)
Definition: race_check.cpp:107
source_locationt::source_locationt
source_locationt()
Definition: source_location.h:23
source_locationt::set_case_number
void set_case_number(const irep_idt &number)
Definition: source_location.h:143
optional.h
source_locationt::set_line
void set_line(unsigned line)
Definition: source_location.h:107
diagnostics_helpert< source_locationt >::diagnostics_as_string
static std::string diagnostics_as_string(const source_locationt &source_location)
Definition: source_location.h:201
source_locationt::nil
static const source_locationt & nil()
Definition: source_location.h:184
prefix.h
file
Definition: kdev_t.h:19
source_locationt::set_java_bytecode_index
void set_java_bytecode_index(const irep_idt &index)
Definition: source_location.h:148
source_locationt::get_column
const irep_idt & get_column() const
Definition: source_location.h:52
source_locationt::set_property_id
void set_property_id(const irep_idt &property_id)
Definition: source_location.h:127
invariant.h
source_locationt::is_built_in
bool is_built_in() const
Definition: source_location.h:175
source_locationt::is_built_in
static bool is_built_in(const std::string &s)
Definition: source_location.h:168
source_locationt::set_working_directory
void set_working_directory(const irep_idt &cwd)
Definition: source_location.h:97
source_locationt::get_line
const irep_idt & get_line() const
Definition: source_location.h:47
source_locationt::set_column
void set_column(const irep_idt &column)
Definition: source_location.h:112
source_locationt::set_line
void set_line(const irep_idt &line)
Definition: source_location.h:102
irept::get_bool
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:239
source_locationt::get_case_number
const irep_idt & get_case_number() const
Definition: source_location.h:77
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
source_locationt::merge
void merge(const source_locationt &from)
Set all unset source-location fields in this object to their values in 'from'.
Definition: source_location.cpp:65
source_locationt::set_file
void set_file(const irep_idt &file)
Definition: source_location.h:92
source_locationt::get_basic_block_covered_lines
const irep_idt & get_basic_block_covered_lines() const
Definition: source_location.h:87
source_locationt::full_path
optionalt< std::string > full_path() const
Get a path to the file, including working directory.
Definition: source_location.cpp:77
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
diagnostics_helpert
Helper to give us some diagnostic in a usable form on assertion failure.
Definition: invariant.h:273
source_locationt
Definition: source_location.h:20
operator<<
std::ostream & operator<<(std::ostream &, const source_locationt &)
Definition: source_location.cpp:87
source_locationt::get_java_bytecode_index
const irep_idt & get_java_bytecode_index() const
Definition: source_location.h:82
source_locationt::get_hide
bool get_hide() const
Definition: source_location.h:163
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:212
source_locationt::set_hide
void set_hide()
Definition: source_location.h:158
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:286
source_locationt::as_string_with_cwd
std::string as_string_with_cwd() const
Definition: source_location.h:32
source_locationt::get_file
const irep_idt & get_file() const
Definition: source_location.h:37
source_locationt::set_column
void set_column(unsigned column)
Definition: source_location.h:117
has_prefix
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
irept
Base class for tree-like data structures with sharing.
Definition: irep.h:156
get_nil_irep
const irept & get_nil_irep()
Definition: irep.cpp:55
source_locationt::set_basic_block_covered_lines
void set_basic_block_covered_lines(const irep_idt &covered_lines)
Definition: source_location.h:153
source_locationt::get_working_directory
const irep_idt & get_working_directory() const
Definition: source_location.h:42
irep.h
source_locationt::set_property_class
void set_property_class(const irep_idt &property_class)
Definition: source_location.h:132