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