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 "irep.h"
14 #include "optional.h"
15 
16 #include <string>
17 
18 class source_locationt:public irept
19 {
20 public:
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 
60  const irep_idt &get_property_id() const
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 
75  const irep_idt &get_case_number() const
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 
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
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
source_locationt::get_function
const irep_idt & get_function() const
Definition: source_location.h:55
source_locationt::get_comment
const irep_idt & get_comment() const
Definition: source_location.h:70
source_locationt::get_property_id
const irep_idt & get_property_id() const
Definition: source_location.h:60
source_locationt::get_property_class
const irep_idt & get_property_class() const
Definition: source_location.h:65
source_locationt::as_string
std::string as_string() const
Definition: source_location.h:25
source_locationt::set_comment
void set_comment(const irep_idt &comment)
Definition: source_location.h:140
source_locationt::set_function
void set_function(const irep_idt &function)
Definition: source_location.h:125
source_locationt::source_locationt
source_locationt()
Definition: source_location.h:21
source_locationt::get_pragmas
const irept::named_subt & get_pragmas() const
Definition: source_location.h:199
source_locationt::set_case_number
void set_case_number(const irep_idt &number)
Definition: source_location.h:146
optional.h
source_locationt::set_line
void set_line(unsigned line)
Definition: source_location.h:110
irept::add
irept & add(const irep_namet &name)
Definition: irep.cpp:116
diagnostics_helpert< source_locationt >::diagnostics_as_string
static std::string diagnostics_as_string(const source_locationt &source_location)
Definition: source_location.h:214
source_locationt::nil
static const source_locationt & nil()
Definition: source_location.h:187
irept::find
const irept & find(const irep_namet &name) const
Definition: irep.cpp:106
file
Definition: kdev_t.h:19
source_locationt::add_pragma
void add_pragma(const irep_idt &pragma)
Definition: source_location.h:194
source_locationt::set_java_bytecode_index
void set_java_bytecode_index(const irep_idt &index)
Definition: source_location.h:151
source_locationt::get_column
const irep_idt & get_column() const
Definition: source_location.h:50
source_locationt::set_property_id
void set_property_id(const irep_idt &property_id)
Definition: source_location.h:130
source_locationt::set_basic_block_source_lines
void set_basic_block_source_lines(const irep_idt &source_lines)
Definition: source_location.h:161
sharing_treet< irept, forward_list_as_mapt< irep_namet, irept > >::named_subt
typename dt::named_subt named_subt
Definition: irep.h:172
source_locationt::is_built_in
bool is_built_in() const
Definition: source_location.h:178
source_locationt::set_working_directory
void set_working_directory(const irep_idt &cwd)
Definition: source_location.h:100
source_locationt::get_basic_block_source_lines
const irep_idt & get_basic_block_source_lines() const
Definition: source_location.h:90
source_locationt::get_line
const irep_idt & get_line() const
Definition: source_location.h:45
source_locationt::set_column
void set_column(const irep_idt &column)
Definition: source_location.h:115
source_locationt::set_line
void set_line(const irep_idt &line)
Definition: source_location.h:105
irept::get_bool
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:58
source_locationt::get_case_number
const irep_idt & get_case_number() const
Definition: source_location.h:75
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
irept::get_named_sub
named_subt & get_named_sub()
Definition: irep.h:469
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:73
source_locationt::set_file
void set_file(const irep_idt &file)
Definition: source_location.h:95
source_locationt::get_basic_block_covered_lines
const irep_idt & get_basic_block_covered_lines() const
Definition: source_location.h:85
source_locationt::full_path
optionalt< std::string > full_path() const
Get a path to the file, including working directory.
Definition: source_location.cpp:85
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:299
source_locationt
Definition: source_location.h:19
operator<<
std::ostream & operator<<(std::ostream &, const source_locationt &)
Definition: source_location.cpp:95
source_locationt::get_java_bytecode_index
const irep_idt & get_java_bytecode_index() const
Definition: source_location.h:80
source_locationt::get_hide
bool get_hide() const
Definition: source_location.h:171
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:45
source_locationt::set_hide
void set_hide()
Definition: source_location.h:166
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:431
source_locationt::as_string_with_cwd
std::string as_string_with_cwd() const
Definition: source_location.h:30
source_locationt::get_file
const irep_idt & get_file() const
Definition: source_location.h:35
source_locationt::set_column
void set_column(unsigned column)
Definition: source_location.h:120
irept
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:383
get_nil_irep
const irept & get_nil_irep()
Definition: irep.cpp:20
source_locationt::set_basic_block_covered_lines
void set_basic_block_covered_lines(const irep_idt &covered_lines)
Definition: source_location.h:156
source_locationt::get_working_directory
const irep_idt & get_working_directory() const
Definition: source_location.h:40
comment
static std::string comment(const rw_set_baset::entryt &entry, bool write)
Definition: race_check.cpp:109
irep.h
source_locationt::set_property_class
void set_property_class(const irep_idt &property_class)
Definition: source_location.h:135