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 
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  const irep_idt &get_function() const
57  {
58  return get(ID_function);
59  }
60 
61  const irep_idt &get_property_id() const
62  {
63  return get(ID_property_id);
64  }
65 
67  {
68  return get(ID_property_class);
69  }
70 
71  const irep_idt &get_comment() const
72  {
73  return get(ID_comment);
74  }
75 
76  const irep_idt &get_case_number() const
77  {
78  return get(ID_switch_case_number);
79  }
80 
82  {
83  return get(ID_java_bytecode_index);
84  }
85 
87  {
88  return get(ID_basic_block_covered_lines);
89  }
90 
92  {
93  return get(ID_basic_block_source_lines);
94  }
95 
96  void set_file(const irep_idt &file)
97  {
98  set(ID_file, file);
99  }
100 
102  {
103  set(ID_working_directory, cwd);
104  }
105 
106  void set_line(const irep_idt &line)
107  {
108  set(ID_line, line);
109  }
110 
111  void set_line(unsigned line)
112  {
113  set(ID_line, line);
114  }
115 
116  void set_column(const irep_idt &column)
117  {
118  set(ID_column, column);
119  }
120 
121  void set_column(unsigned column)
122  {
123  set(ID_column, column);
124  }
125 
126  void set_function(const irep_idt &function)
127  {
128  set(ID_function, function);
129  }
130 
131  void set_property_id(const irep_idt &property_id)
132  {
133  set(ID_property_id, property_id);
134  }
135 
136  void set_property_class(const irep_idt &property_class)
137  {
138  set(ID_property_class, property_class);
139  }
140 
142  {
143  set(ID_comment, comment);
144  }
145 
146  // for switch case number
147  void set_case_number(const irep_idt &number)
148  {
149  set(ID_switch_case_number, number);
150  }
151 
153  {
154  set(ID_java_bytecode_index, index);
155  }
156 
157  void set_basic_block_covered_lines(const irep_idt &covered_lines)
158  {
159  return set(ID_basic_block_covered_lines, covered_lines);
160  }
161 
162  void set_basic_block_source_lines(const irep_idt &source_lines)
163  {
164  return set(ID_basic_block_source_lines, source_lines);
165  }
166 
167  void set_hide()
168  {
169  set(ID_hide, true);
170  }
171 
172  bool get_hide() const
173  {
174  return get_bool(ID_hide);
175  }
176 
177  static bool is_built_in(const std::string &s);
178 
179  bool is_built_in() const
180  {
181  return is_built_in(id2string(get_file()));
182  }
183 
186  void merge(const source_locationt &from);
187 
188  static const source_locationt &nil()
189  {
190  return static_cast<const source_locationt &>(get_nil_irep());
191  }
192 
194 
195  void add_pragma(const irep_idt &pragma)
196  {
197  add(ID_pragma).add(pragma);
198  }
199 
201  {
202  return find(ID_pragma).get_named_sub();
203  }
204 
205 protected:
206  std::string as_string(bool print_cwd) const;
207 };
208 
209 std::ostream &operator <<(std::ostream &, const source_locationt &);
210 
211 template <>
213 {
214  static std::string
215  diagnostics_as_string(const source_locationt &source_location)
216  {
217  return "source location: " + source_location.as_string();
218  }
219 };
220 
221 #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:36
source_locationt::get_function
const irep_idt & get_function() const
Definition: source_location.h:56
source_locationt::get_comment
const irep_idt & get_comment() const
Definition: source_location.h:71
source_locationt::get_property_id
const irep_idt & get_property_id() const
Definition: source_location.h:61
source_locationt::get_property_class
const irep_idt & get_property_class() const
Definition: source_location.h:66
source_locationt::as_string
std::string as_string() const
Definition: source_location.h:26
source_locationt::set_comment
void set_comment(const irep_idt &comment)
Definition: source_location.h:141
source_locationt::set_function
void set_function(const irep_idt &function)
Definition: source_location.h:126
source_locationt::source_locationt
source_locationt()
Definition: source_location.h:22
source_locationt::get_pragmas
const irept::named_subt & get_pragmas() const
Definition: source_location.h:200
source_locationt::set_case_number
void set_case_number(const irep_idt &number)
Definition: source_location.h:147
optional.h
source_locationt::set_line
void set_line(unsigned line)
Definition: source_location.h:111
irept::add
irept & add(const irep_namet &name)
Definition: irep.cpp:113
diagnostics_helpert< source_locationt >::diagnostics_as_string
static std::string diagnostics_as_string(const source_locationt &source_location)
Definition: source_location.h:215
source_locationt::nil
static const source_locationt & nil()
Definition: source_location.h:188
irept::find
const irept & find(const irep_namet &name) const
Definition: irep.cpp:103
file
Definition: kdev_t.h:19
invariant.h
source_locationt::add_pragma
void add_pragma(const irep_idt &pragma)
Definition: source_location.h:195
source_locationt::set_java_bytecode_index
void set_java_bytecode_index(const irep_idt &index)
Definition: source_location.h:152
source_locationt::get_column
const irep_idt & get_column() const
Definition: source_location.h:51
source_locationt::set_property_id
void set_property_id(const irep_idt &property_id)
Definition: source_location.h:131
source_locationt::set_basic_block_source_lines
void set_basic_block_source_lines(const irep_idt &source_lines)
Definition: source_location.h:162
sharing_treet< irept, std::map< irep_namet, irept > >::named_subt
typename dt::named_subt named_subt
Definition: irep.h:183
source_locationt::is_built_in
bool is_built_in() const
Definition: source_location.h:179
source_locationt::set_working_directory
void set_working_directory(const irep_idt &cwd)
Definition: source_location.h:101
source_locationt::get_basic_block_source_lines
const irep_idt & get_basic_block_source_lines() const
Definition: source_location.h:91
source_locationt::get_line
const irep_idt & get_line() const
Definition: source_location.h:46
source_locationt::set_column
void set_column(const irep_idt &column)
Definition: source_location.h:116
source_locationt::set_line
void set_line(const irep_idt &line)
Definition: source_location.h:106
irept::get_bool
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:64
source_locationt::get_case_number
const irep_idt & get_case_number() const
Definition: source_location.h:76
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
irept::get_named_sub
named_subt & get_named_sub()
Definition: irep.h:479
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:96
source_locationt::get_basic_block_covered_lines
const irep_idt & get_basic_block_covered_lines() const
Definition: source_location.h:86
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:81
source_locationt::get_hide
bool get_hide() const
Definition: source_location.h:172
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:51
source_locationt::set_hide
void set_hide()
Definition: source_location.h:167
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:442
source_locationt::as_string_with_cwd
std::string as_string_with_cwd() const
Definition: source_location.h:31
source_locationt::get_file
const irep_idt & get_file() const
Definition: source_location.h:36
source_locationt::set_column
void set_column(unsigned column)
Definition: source_location.h:121
irept
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:381
get_nil_irep
const irept & get_nil_irep()
Definition: irep.cpp:26
source_locationt::set_basic_block_covered_lines
void set_basic_block_covered_lines(const irep_idt &covered_lines)
Definition: source_location.h:157
source_locationt::get_working_directory
const irep_idt & get_working_directory() const
Definition: source_location.h:41
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:136