cprover
pointer_offset_size.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Pointer Logic
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "pointer_offset_size.h"
13 
14 #include "arith_tools.h"
15 #include "byte_operators.h"
16 #include "c_types.h"
17 #include "invariant.h"
18 #include "namespace.h"
19 #include "simplify_expr.h"
20 #include "ssa_expr.h"
21 #include "std_expr.h"
22 
24  const struct_typet &type,
25  const irep_idt &member,
26  const namespacet &ns)
27 {
28  mp_integer result = 0;
29  std::size_t bit_field_bits = 0;
30 
31  for(const auto &comp : type.components())
32  {
33  if(comp.get_name() == member)
34  return result;
35 
36  if(comp.type().id() == ID_c_bit_field)
37  {
38  const std::size_t w = to_c_bit_field_type(comp.type()).get_width();
39  bit_field_bits += w;
40  result += bit_field_bits / 8;
41  bit_field_bits %= 8;
42  }
43  else if(comp.type().id() == ID_bool)
44  {
45  ++bit_field_bits;
46  result += bit_field_bits / 8;
47  bit_field_bits %= 8;
48  }
49  else
50  {
52  bit_field_bits == 0, "padding ensures offset at byte boundaries");
53  const auto sub_size = pointer_offset_size(comp.type(), ns);
54  if(!sub_size.has_value())
55  return {};
56  else
57  result += *sub_size;
58  }
59  }
60 
61  return result;
62 }
63 
65  const struct_typet &type,
66  const irep_idt &member,
67  const namespacet &ns)
68 {
69  mp_integer offset=0;
70  const struct_typet::componentst &components=type.components();
71 
72  for(const auto &comp : components)
73  {
74  if(comp.get_name()==member)
75  return offset;
76 
77  auto member_bits = pointer_offset_bits(comp.type(), ns);
78  if(!member_bits.has_value())
79  return {};
80 
81  offset += *member_bits;
82  }
83 
84  return {};
85 }
86 
89 pointer_offset_size(const typet &type, const namespacet &ns)
90 {
91  auto bits = pointer_offset_bits(type, ns);
92 
93  if(bits.has_value())
94  return (*bits + 7) / 8;
95  else
96  return {};
97 }
98 
100 pointer_offset_bits(const typet &type, const namespacet &ns)
101 {
102  if(type.id()==ID_array)
103  {
104  auto sub = pointer_offset_bits(to_array_type(type).subtype(), ns);
105  if(!sub.has_value())
106  return {};
107 
108  // get size - we can only distinguish the elements if the size is constant
109  const auto size = numeric_cast<mp_integer>(to_array_type(type).size());
110  if(!size.has_value())
111  return {};
112 
113  return (*sub) * (*size);
114  }
115  else if(type.id()==ID_vector)
116  {
117  auto sub = pointer_offset_bits(to_vector_type(type).subtype(), ns);
118  if(!sub.has_value())
119  return {};
120 
121  // get size
122  const mp_integer size =
123  numeric_cast_v<mp_integer>(to_vector_type(type).size());
124 
125  return (*sub) * size;
126  }
127  else if(type.id()==ID_complex)
128  {
129  auto sub = pointer_offset_bits(to_complex_type(type).subtype(), ns);
130 
131  if(sub.has_value())
132  return (*sub) * 2;
133  else
134  return {};
135  }
136  else if(type.id()==ID_struct)
137  {
138  const struct_typet &struct_type=to_struct_type(type);
139  mp_integer result=0;
140 
141  for(const auto &c : struct_type.components())
142  {
143  const typet &subtype = c.type();
144  auto sub_size = pointer_offset_bits(subtype, ns);
145 
146  if(!sub_size.has_value())
147  return {};
148 
149  result += *sub_size;
150  }
151 
152  return result;
153  }
154  else if(type.id()==ID_union)
155  {
156  const union_typet &union_type=to_union_type(type);
157 
158  if(union_type.components().empty())
159  return mp_integer{0};
160 
161  const auto widest_member = union_type.find_widest_union_component(ns);
162 
163  if(widest_member.has_value())
164  return widest_member->second;
165  else
166  return {};
167  }
168  else if(type.id()==ID_signedbv ||
169  type.id()==ID_unsignedbv ||
170  type.id()==ID_fixedbv ||
171  type.id()==ID_floatbv ||
172  type.id()==ID_bv ||
173  type.id()==ID_c_bool ||
174  type.id()==ID_c_bit_field)
175  {
176  return mp_integer(to_bitvector_type(type).get_width());
177  }
178  else if(type.id()==ID_c_enum)
179  {
180  return mp_integer(to_bitvector_type(to_c_enum_type(type).subtype()).get_width());
181  }
182  else if(type.id()==ID_c_enum_tag)
183  {
184  return pointer_offset_bits(ns.follow_tag(to_c_enum_tag_type(type)), ns);
185  }
186  else if(type.id()==ID_bool)
187  {
188  return mp_integer(1);
189  }
190  else if(type.id()==ID_pointer)
191  {
192  // the following is an MS extension
193  if(type.get_bool(ID_C_ptr32))
194  return mp_integer(32);
195 
196  return mp_integer(to_bitvector_type(type).get_width());
197  }
198  else if(type.id() == ID_union_tag)
199  {
200  return pointer_offset_bits(ns.follow_tag(to_union_tag_type(type)), ns);
201  }
202  else if(type.id() == ID_struct_tag)
203  {
204  return pointer_offset_bits(ns.follow_tag(to_struct_tag_type(type)), ns);
205  }
206  else if(type.id()==ID_code)
207  {
208  return mp_integer(0);
209  }
210  else if(type.id()==ID_string)
211  {
212  return mp_integer(32);
213  }
214  else
215  return {};
216 }
217 
219 member_offset_expr(const member_exprt &member_expr, const namespacet &ns)
220 {
221  // need to distinguish structs and unions
222  const typet &type=ns.follow(member_expr.struct_op().type());
223  if(type.id()==ID_struct)
224  return member_offset_expr(
225  to_struct_type(type), member_expr.get_component_name(), ns);
226  else if(type.id()==ID_union)
227  return from_integer(0, size_type());
228  else
229  return {};
230 }
231 
233  const struct_typet &type,
234  const irep_idt &member,
235  const namespacet &ns)
236 {
237  PRECONDITION(size_type().get_width() != 0);
238  exprt result=from_integer(0, size_type());
239  std::size_t bit_field_bits=0;
240 
241  for(const auto &c : type.components())
242  {
243  if(c.get_name() == member)
244  break;
245 
246  if(c.type().id() == ID_c_bit_field)
247  {
248  std::size_t w = to_c_bit_field_type(c.type()).get_width();
249  bit_field_bits += w;
250  const std::size_t bytes = bit_field_bits / 8;
251  bit_field_bits %= 8;
252  if(bytes > 0)
253  result = plus_exprt(result, from_integer(bytes, result.type()));
254  }
255  else if(c.type().id() == ID_bool)
256  {
257  ++bit_field_bits;
258  const std::size_t bytes = bit_field_bits / 8;
259  bit_field_bits %= 8;
260  if(bytes > 0)
261  result = plus_exprt(result, from_integer(bytes, result.type()));
262  }
263  else
264  {
266  bit_field_bits == 0, "padding ensures offset at byte boundaries");
267  const typet &subtype = c.type();
268  auto sub_size = size_of_expr(subtype, ns);
269  if(!sub_size.has_value())
270  return {}; // give up
271  result = plus_exprt(result, sub_size.value());
272  }
273  }
274 
275  return simplify_expr(std::move(result), ns);
276 }
277 
279 {
280  if(type.id()==ID_array)
281  {
282  const auto &array_type = to_array_type(type);
283 
284  // special-case arrays of bits
285  if(array_type.subtype().id() == ID_bool)
286  {
287  auto bits = pointer_offset_bits(array_type, ns);
288 
289  if(bits.has_value())
290  return from_integer((*bits + 7) / 8, size_type());
291  }
292 
293  auto sub = size_of_expr(array_type.subtype(), ns);
294  if(!sub.has_value())
295  return {};
296 
297  const exprt &size = array_type.size();
298 
299  if(size.is_nil())
300  return {};
301 
302  const auto size_casted =
303  typecast_exprt::conditional_cast(size, sub.value().type());
304 
305  return simplify_expr(mult_exprt{size_casted, sub.value()}, ns);
306  }
307  else if(type.id()==ID_vector)
308  {
309  const auto &vector_type = to_vector_type(type);
310 
311  // special-case vectors of bits
312  if(vector_type.subtype().id() == ID_bool)
313  {
314  auto bits = pointer_offset_bits(vector_type, ns);
315 
316  if(bits.has_value())
317  return from_integer((*bits + 7) / 8, size_type());
318  }
319 
320  auto sub = size_of_expr(vector_type.subtype(), ns);
321  if(!sub.has_value())
322  return {};
323 
324  const exprt &size = to_vector_type(type).size();
325 
326  if(size.is_nil())
327  return {};
328 
329  const auto size_casted =
330  typecast_exprt::conditional_cast(size, sub.value().type());
331 
332  return simplify_expr(mult_exprt{size_casted, sub.value()}, ns);
333  }
334  else if(type.id()==ID_complex)
335  {
336  auto sub = size_of_expr(to_complex_type(type).subtype(), ns);
337  if(!sub.has_value())
338  return {};
339 
340  exprt size = from_integer(2, sub.value().type());
341  return simplify_expr(mult_exprt{std::move(size), sub.value()}, ns);
342  }
343  else if(type.id()==ID_struct)
344  {
345  const struct_typet &struct_type=to_struct_type(type);
346 
347  exprt result=from_integer(0, size_type());
348  std::size_t bit_field_bits=0;
349 
350  for(const auto &c : struct_type.components())
351  {
352  if(c.type().id() == ID_c_bit_field)
353  {
354  std::size_t w = to_c_bit_field_type(c.type()).get_width();
355  bit_field_bits += w;
356  const std::size_t bytes = bit_field_bits / 8;
357  bit_field_bits %= 8;
358  if(bytes > 0)
359  result = plus_exprt(result, from_integer(bytes, result.type()));
360  }
361  else if(c.type().id() == ID_bool)
362  {
363  ++bit_field_bits;
364  const std::size_t bytes = bit_field_bits / 8;
365  bit_field_bits %= 8;
366  if(bytes > 0)
367  result = plus_exprt(result, from_integer(bytes, result.type()));
368  }
369  else
370  {
372  bit_field_bits == 0, "padding ensures offset at byte boundaries");
373  const typet &subtype = c.type();
374  auto sub_size_opt = size_of_expr(subtype, ns);
375  if(!sub_size_opt.has_value())
376  return {};
377 
378  result = plus_exprt(result, sub_size_opt.value());
379  }
380  }
381 
382  return simplify_expr(std::move(result), ns);
383  }
384  else if(type.id()==ID_union)
385  {
386  const union_typet &union_type=to_union_type(type);
387 
388  mp_integer max_bytes=0;
389  exprt result=from_integer(0, size_type());
390 
391  // compute max
392 
393  for(const auto &c : union_type.components())
394  {
395  const typet &subtype = c.type();
396  exprt sub_size;
397 
398  auto sub_bits = pointer_offset_bits(subtype, ns);
399 
400  if(!sub_bits.has_value())
401  {
402  max_bytes=-1;
403 
404  auto sub_size_opt = size_of_expr(subtype, ns);
405  if(!sub_size_opt.has_value())
406  return {};
407  sub_size = sub_size_opt.value();
408  }
409  else
410  {
411  mp_integer sub_bytes = (*sub_bits + 7) / 8;
412 
413  if(max_bytes>=0)
414  {
415  if(max_bytes<sub_bytes)
416  {
417  max_bytes=sub_bytes;
418  result=from_integer(sub_bytes, size_type());
419  }
420 
421  continue;
422  }
423 
424  sub_size=from_integer(sub_bytes, size_type());
425  }
426 
427  result=if_exprt(
428  binary_relation_exprt(result, ID_lt, sub_size),
429  sub_size, result);
430 
431  simplify(result, ns);
432  }
433 
434  return result;
435  }
436  else if(type.id()==ID_signedbv ||
437  type.id()==ID_unsignedbv ||
438  type.id()==ID_fixedbv ||
439  type.id()==ID_floatbv ||
440  type.id()==ID_bv ||
441  type.id()==ID_c_bool ||
442  type.id()==ID_c_bit_field)
443  {
444  std::size_t width=to_bitvector_type(type).get_width();
445  std::size_t bytes=width/8;
446  if(bytes*8!=width)
447  bytes++;
448  return from_integer(bytes, size_type());
449  }
450  else if(type.id()==ID_c_enum)
451  {
452  std::size_t width =
453  to_bitvector_type(to_c_enum_type(type).subtype()).get_width();
454  std::size_t bytes=width/8;
455  if(bytes*8!=width)
456  bytes++;
457  return from_integer(bytes, size_type());
458  }
459  else if(type.id()==ID_c_enum_tag)
460  {
461  return size_of_expr(ns.follow_tag(to_c_enum_tag_type(type)), ns);
462  }
463  else if(type.id()==ID_bool)
464  {
465  return from_integer(1, size_type());
466  }
467  else if(type.id()==ID_pointer)
468  {
469  // the following is an MS extension
470  if(type.get_bool(ID_C_ptr32))
471  return from_integer(4, size_type());
472 
473  std::size_t width=to_bitvector_type(type).get_width();
474  std::size_t bytes=width/8;
475  if(bytes*8!=width)
476  bytes++;
477  return from_integer(bytes, size_type());
478  }
479  else if(type.id() == ID_union_tag)
480  {
481  return size_of_expr(ns.follow_tag(to_union_tag_type(type)), ns);
482  }
483  else if(type.id() == ID_struct_tag)
484  {
485  return size_of_expr(ns.follow_tag(to_struct_tag_type(type)), ns);
486  }
487  else if(type.id()==ID_code)
488  {
489  return from_integer(0, size_type());
490  }
491  else if(type.id()==ID_string)
492  {
493  return from_integer(32/8, size_type());
494  }
495  else
496  return {};
497 }
498 
500 compute_pointer_offset(const exprt &expr, const namespacet &ns)
501 {
502  if(expr.id()==ID_symbol)
503  {
504  if(is_ssa_expr(expr))
505  return compute_pointer_offset(
506  to_ssa_expr(expr).get_original_expr(), ns);
507  else
508  return mp_integer(0);
509  }
510  else if(expr.id()==ID_index)
511  {
512  const index_exprt &index_expr=to_index_expr(expr);
514  index_expr.array().type().id() == ID_array,
515  "index into array expected, found " +
516  index_expr.array().type().id_string());
517 
518  auto o = compute_pointer_offset(index_expr.array(), ns);
519 
520  if(o.has_value())
521  {
522  const auto &array_type = to_array_type(index_expr.array().type());
523  auto sub_size = pointer_offset_size(array_type.subtype(), ns);
524 
525  if(sub_size.has_value() && *sub_size > 0)
526  {
527  const auto i = numeric_cast<mp_integer>(index_expr.index());
528  if(i.has_value())
529  return (*o) + (*i) * (*sub_size);
530  }
531  }
532 
533  // don't know
534  }
535  else if(expr.id()==ID_member)
536  {
537  const member_exprt &member_expr=to_member_expr(expr);
538  const exprt &op=member_expr.struct_op();
539  const struct_union_typet &type=to_struct_union_type(ns.follow(op.type()));
540 
541  auto o = compute_pointer_offset(op, ns);
542 
543  if(o.has_value())
544  {
545  if(type.id()==ID_union)
546  return *o;
547 
549  to_struct_type(type), member_expr.get_component_name(), ns);
550 
551  if(member_offset.has_value())
552  return *o + *member_offset;
553  }
554  }
555  else if(expr.id()==ID_string_constant)
556  return mp_integer(0);
557 
558  return {}; // don't know
559 }
560 
563 {
564  const typet &type=
565  static_cast<const typet &>(expr.find(ID_C_c_sizeof_type));
566 
567  if(type.is_nil())
568  return {};
569 
570  const auto type_size = pointer_offset_size(type, ns);
571  auto val = numeric_cast<mp_integer>(expr);
572 
573  if(
574  !type_size.has_value() || *type_size < 0 || !val.has_value() ||
575  *val < *type_size || (*type_size == 0 && *val > 0))
576  {
577  return {};
578  }
579 
580  const typet t(size_type());
582  address_bits(*val + 1) <= *pointer_offset_bits(t, ns),
583  "sizeof value does not fit size_type");
584 
585  mp_integer remainder=0;
586 
587  if(*type_size != 0)
588  {
589  remainder = *val % *type_size;
590  *val -= remainder;
591  *val /= *type_size;
592  }
593 
594  exprt result(ID_sizeof, t);
595  result.set(ID_type_arg, type);
596 
597  if(*val > 1)
598  result = mult_exprt(result, from_integer(*val, t));
599  if(remainder>0)
600  result=plus_exprt(result, from_integer(remainder, t));
601 
602  return typecast_exprt::conditional_cast(result, expr.type());
603 }
604 
606  const exprt &expr,
607  const mp_integer &offset_bytes,
608  const typet &target_type_raw,
609  const namespacet &ns)
610 {
611  if(offset_bytes == 0 && expr.type() == target_type_raw)
612  {
613  exprt result = expr;
614 
615  if(expr.type() != target_type_raw)
616  result.type() = target_type_raw;
617 
618  return result;
619  }
620 
621  if(
622  offset_bytes == 0 && expr.type().id() == ID_pointer &&
623  target_type_raw.id() == ID_pointer)
624  {
625  return typecast_exprt(expr, target_type_raw);
626  }
627 
628  const typet &source_type = ns.follow(expr.type());
629  const auto target_size_bits = pointer_offset_bits(target_type_raw, ns);
630  if(!target_size_bits.has_value())
631  return {};
632 
633  if(source_type.id()==ID_struct)
634  {
635  const struct_typet &struct_type = to_struct_type(source_type);
636 
637  mp_integer m_offset_bits = 0;
638  for(const auto &component : struct_type.components())
639  {
640  const auto m_size_bits = pointer_offset_bits(component.type(), ns);
641  if(!m_size_bits.has_value())
642  return {};
643 
644  // if this member completely contains the target, and this member is
645  // byte-aligned, recurse into it
646  if(
647  offset_bytes * 8 >= m_offset_bits && m_offset_bits % 8 == 0 &&
648  offset_bytes * 8 + *target_size_bits <= m_offset_bits + *m_size_bits)
649  {
650  const member_exprt member(expr, component.get_name(), component.type());
652  member, offset_bytes - m_offset_bits / 8, target_type_raw, ns);
653  }
654 
655  m_offset_bits += *m_size_bits;
656  }
657  }
658  else if(source_type.id()==ID_array)
659  {
660  const array_typet &array_type = to_array_type(source_type);
661 
662  const auto elem_size_bits = pointer_offset_bits(array_type.subtype(), ns);
663 
664  // no arrays of non-byte-aligned, zero-, or unknown-sized objects
665  if(
666  elem_size_bits.has_value() && *elem_size_bits > 0 &&
667  *elem_size_bits % 8 == 0 && *target_size_bits <= *elem_size_bits)
668  {
669  const mp_integer elem_size_bytes = *elem_size_bits / 8;
670  const auto offset_inside_elem = offset_bytes % elem_size_bytes;
671  const auto target_size_bytes = *target_size_bits / 8;
672  // only recurse if the cell completely contains the target
673  if(offset_inside_elem + target_size_bytes <= elem_size_bytes)
674  {
676  index_exprt(
677  expr, from_integer(offset_bytes / elem_size_bytes, index_type())),
678  offset_inside_elem,
679  target_type_raw,
680  ns);
681  }
682  }
683  }
684 
685  return byte_extract_exprt(
686  byte_extract_id(),
687  expr,
688  from_integer(offset_bytes, index_type()),
689  target_type_raw);
690 }
691 
693  const exprt &expr,
694  const exprt &offset,
695  const typet &target_type,
696  const namespacet &ns)
697 {
698  const auto offset_bytes = numeric_cast<mp_integer>(offset);
699 
700  if(!offset_bytes.has_value())
701  return {};
702  else
703  return get_subexpression_at_offset(expr, *offset_bytes, target_type, ns);
704 }
to_union_tag_type
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition: c_types.h:189
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:141
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
pointer_offset_size.h
Pointer Logic.
to_union_type
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition: c_types.h:149
typecast_exprt::conditional_cast
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:1788
typet::subtype
const typet & subtype() const
Definition: type.h:47
arith_tools.h
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:302
to_struct_union_type
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Definition: std_types.h:208
member_offset_bits
optionalt< mp_integer > member_offset_bits(const struct_typet &type, const irep_idt &member, const namespacet &ns)
Definition: pointer_offset_size.cpp:64
typet
The type of an expression, extends irept.
Definition: type.h:28
union_typet::find_widest_union_component
optionalt< std::pair< struct_union_typet::componentt, mp_integer > > find_widest_union_component(const namespacet &ns) const
Determine the member of maximum bit width in a union type.
Definition: c_types.cpp:308
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1296
struct_union_typet
Base type for structs and unions.
Definition: std_types.h:56
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:2086
to_c_enum_type
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
Definition: c_types.h:277
irept::find
const irept & find(const irep_namet &name) const
Definition: irep.cpp:112
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:830
exprt
Base class for all expressions.
Definition: expr.h:54
struct_union_typet::componentst
std::vector< componentt > componentst
Definition: std_types.h:134
namespace_baset::follow_tag
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:66
component
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:55
to_bitvector_type
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
Definition: bitvector_types.h:32
to_complex_type
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
Definition: std_types.h:1034
namespace.h
index_type
bitvector_typet index_type()
Definition: c_types.cpp:16
address_bits
std::size_t address_bits(const mp_integer &size)
ceil(log2(size))
Definition: arith_tools.cpp:177
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
compute_pointer_offset
optionalt< mp_integer > compute_pointer_offset(const exprt &expr, const namespacet &ns)
Definition: pointer_offset_size.cpp:500
byte_extract_id
irep_idt byte_extract_id()
Definition: byte_operators.cpp:13
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
irept::get_bool
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:64
byte_operators.h
Expression classes for byte-level operators.
is_ssa_expr
bool is_ssa_expr(const exprt &expr)
Definition: ssa_expr.h:125
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
to_ssa_expr
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition: ssa_expr.h:145
to_c_enum_tag_type
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
Definition: c_types.h:317
member_exprt::struct_op
const exprt & struct_op() const
Definition: std_expr.h:2557
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
pointer_offset_bits
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
Definition: pointer_offset_size.cpp:100
irept::id_string
const std::string & id_string() const
Definition: irep.h:410
simplify
bool simplify(exprt &expr, const namespacet &ns)
Definition: simplify_expr.cpp:2552
mult_exprt
Binary multiplication Associativity is not specified.
Definition: std_expr.h:935
simplify_expr
exprt simplify_expr(exprt src, const namespacet &ns)
Definition: simplify_expr.cpp:2557
index_exprt::index
exprt & index()
Definition: std_expr.h:1268
index_exprt::array
exprt & array()
Definition: std_expr.h:1258
irept::is_nil
bool is_nil() const
Definition: irep.h:387
irept::id
const irep_idt & id() const
Definition: irep.h:407
to_struct_tag_type
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:468
union_typet
The union type.
Definition: c_types.h:112
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
vector_typet::size
const constant_exprt & size() const
Definition: std_types.cpp:243
simplify_expr.h
bitvector_typet::get_width
std::size_t get_width() const
Definition: std_types.h:837
member_exprt
Extract member of struct or union.
Definition: std_expr.h:2527
to_c_bit_field_type
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a typet to a c_bit_field_typet.
Definition: c_types.h:47
ssa_expr.h
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:225
pointer_offset_size
optionalt< mp_integer > pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
Definition: pointer_offset_size.cpp:89
array_typet
Arrays with given size.
Definition: std_types.h:757
build_sizeof_expr
optionalt< exprt > build_sizeof_expr(const constant_exprt &expr, const namespacet &ns)
Definition: pointer_offset_size.cpp:562
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:52
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:431
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:100
get_subexpression_at_offset
optionalt< exprt > get_subexpression_at_offset(const exprt &expr, const mp_integer &offset_bytes, const typet &target_type_raw, const namespacet &ns)
Definition: pointer_offset_size.cpp:605
binary_relation_exprt
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:674
invariant.h
byte_extract_exprt
Expression of type type extracted from some object op starting at position offset (given in number of...
Definition: byte_operators.h:29
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:807
to_vector_type
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition: std_types.h:994
size_of_expr
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
Definition: pointer_offset_size.cpp:278
to_member_expr
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2611
member_exprt::get_component_name
irep_idt get_component_name() const
Definition: std_expr.h:2541
index_exprt
Array index operator.
Definition: std_expr.h:1242
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:1780
size_type
unsignedbv_typet size_type()
Definition: c_types.cpp:58
constant_exprt
A constant literal expression.
Definition: std_expr.h:2667
member_offset_expr
optionalt< exprt > member_offset_expr(const member_exprt &member_expr, const namespacet &ns)
Definition: pointer_offset_size.cpp:219
std_expr.h
API to expression classes.
member_offset
optionalt< mp_integer > member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
Definition: pointer_offset_size.cpp:23
c_types.h