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  mp_integer result=0;
158 
159  // compute max
160 
161  for(const auto &c : union_type.components())
162  {
163  const typet &subtype = c.type();
164  auto sub_size = pointer_offset_bits(subtype, ns);
165 
166  if(!sub_size.has_value())
167  return {};
168 
169  if(*sub_size > result)
170  result = *sub_size;
171  }
172 
173  return result;
174  }
175  else if(type.id()==ID_signedbv ||
176  type.id()==ID_unsignedbv ||
177  type.id()==ID_fixedbv ||
178  type.id()==ID_floatbv ||
179  type.id()==ID_bv ||
180  type.id()==ID_c_bool ||
181  type.id()==ID_c_bit_field)
182  {
183  return mp_integer(to_bitvector_type(type).get_width());
184  }
185  else if(type.id()==ID_c_enum)
186  {
187  return mp_integer(to_bitvector_type(to_c_enum_type(type).subtype()).get_width());
188  }
189  else if(type.id()==ID_c_enum_tag)
190  {
191  return pointer_offset_bits(ns.follow_tag(to_c_enum_tag_type(type)), ns);
192  }
193  else if(type.id()==ID_bool)
194  {
195  return mp_integer(1);
196  }
197  else if(type.id()==ID_pointer)
198  {
199  // the following is an MS extension
200  if(type.get_bool(ID_C_ptr32))
201  return mp_integer(32);
202 
203  return mp_integer(to_bitvector_type(type).get_width());
204  }
205  else if(type.id() == ID_union_tag)
206  {
207  return pointer_offset_bits(ns.follow_tag(to_union_tag_type(type)), ns);
208  }
209  else if(type.id() == ID_struct_tag)
210  {
211  return pointer_offset_bits(ns.follow_tag(to_struct_tag_type(type)), ns);
212  }
213  else if(type.id()==ID_code)
214  {
215  return mp_integer(0);
216  }
217  else if(type.id()==ID_string)
218  {
219  return mp_integer(32);
220  }
221  else
222  return {};
223 }
224 
226 member_offset_expr(const member_exprt &member_expr, const namespacet &ns)
227 {
228  // need to distinguish structs and unions
229  const typet &type=ns.follow(member_expr.struct_op().type());
230  if(type.id()==ID_struct)
231  return member_offset_expr(
232  to_struct_type(type), member_expr.get_component_name(), ns);
233  else if(type.id()==ID_union)
234  return from_integer(0, size_type());
235  else
236  return {};
237 }
238 
240  const struct_typet &type,
241  const irep_idt &member,
242  const namespacet &ns)
243 {
244  PRECONDITION(size_type().get_width() != 0);
245  exprt result=from_integer(0, size_type());
246  std::size_t bit_field_bits=0;
247 
248  for(const auto &c : type.components())
249  {
250  if(c.get_name() == member)
251  break;
252 
253  if(c.type().id() == ID_c_bit_field)
254  {
255  std::size_t w = to_c_bit_field_type(c.type()).get_width();
256  bit_field_bits += w;
257  const std::size_t bytes = bit_field_bits / 8;
258  bit_field_bits %= 8;
259  if(bytes > 0)
260  result = plus_exprt(result, from_integer(bytes, result.type()));
261  }
262  else if(c.type().id() == ID_bool)
263  {
264  ++bit_field_bits;
265  const std::size_t bytes = bit_field_bits / 8;
266  bit_field_bits %= 8;
267  if(bytes > 0)
268  result = plus_exprt(result, from_integer(bytes, result.type()));
269  }
270  else
271  {
273  bit_field_bits == 0, "padding ensures offset at byte boundaries");
274  const typet &subtype = c.type();
275  auto sub_size = size_of_expr(subtype, ns);
276  if(!sub_size.has_value())
277  return {}; // give up
278  result = plus_exprt(result, sub_size.value());
279  }
280  }
281 
282  return simplify_expr(std::move(result), ns);
283 }
284 
286 {
287  if(type.id()==ID_array)
288  {
289  const auto &array_type = to_array_type(type);
290 
291  // special-case arrays of bits
292  if(array_type.subtype().id() == ID_bool)
293  {
294  auto bits = pointer_offset_bits(array_type, ns);
295 
296  if(bits.has_value())
297  return from_integer((*bits + 7) / 8, size_type());
298  }
299 
300  auto sub = size_of_expr(array_type.subtype(), ns);
301  if(!sub.has_value())
302  return {};
303 
304  const exprt &size = array_type.size();
305 
306  if(size.is_nil())
307  return {};
308 
309  const auto size_casted =
310  typecast_exprt::conditional_cast(size, sub.value().type());
311 
312  return simplify_expr(mult_exprt{size_casted, sub.value()}, ns);
313  }
314  else if(type.id()==ID_vector)
315  {
316  const auto &vector_type = to_vector_type(type);
317 
318  // special-case vectors of bits
319  if(vector_type.subtype().id() == ID_bool)
320  {
321  auto bits = pointer_offset_bits(vector_type, ns);
322 
323  if(bits.has_value())
324  return from_integer((*bits + 7) / 8, size_type());
325  }
326 
327  auto sub = size_of_expr(vector_type.subtype(), ns);
328  if(!sub.has_value())
329  return {};
330 
331  const exprt &size = to_vector_type(type).size();
332 
333  if(size.is_nil())
334  return {};
335 
336  const auto size_casted =
337  typecast_exprt::conditional_cast(size, sub.value().type());
338 
339  return simplify_expr(mult_exprt{size_casted, sub.value()}, ns);
340  }
341  else if(type.id()==ID_complex)
342  {
343  auto sub = size_of_expr(to_complex_type(type).subtype(), ns);
344  if(!sub.has_value())
345  return {};
346 
347  exprt size = from_integer(2, sub.value().type());
348  return simplify_expr(mult_exprt{std::move(size), sub.value()}, ns);
349  }
350  else if(type.id()==ID_struct)
351  {
352  const struct_typet &struct_type=to_struct_type(type);
353 
354  exprt result=from_integer(0, size_type());
355  std::size_t bit_field_bits=0;
356 
357  for(const auto &c : struct_type.components())
358  {
359  if(c.type().id() == ID_c_bit_field)
360  {
361  std::size_t w = to_c_bit_field_type(c.type()).get_width();
362  bit_field_bits += w;
363  const std::size_t bytes = bit_field_bits / 8;
364  bit_field_bits %= 8;
365  if(bytes > 0)
366  result = plus_exprt(result, from_integer(bytes, result.type()));
367  }
368  else if(c.type().id() == ID_bool)
369  {
370  ++bit_field_bits;
371  const std::size_t bytes = bit_field_bits / 8;
372  bit_field_bits %= 8;
373  if(bytes > 0)
374  result = plus_exprt(result, from_integer(bytes, result.type()));
375  }
376  else
377  {
379  bit_field_bits == 0, "padding ensures offset at byte boundaries");
380  const typet &subtype = c.type();
381  auto sub_size_opt = size_of_expr(subtype, ns);
382  if(!sub_size_opt.has_value())
383  return {};
384 
385  result = plus_exprt(result, sub_size_opt.value());
386  }
387  }
388 
389  return simplify_expr(std::move(result), ns);
390  }
391  else if(type.id()==ID_union)
392  {
393  const union_typet &union_type=to_union_type(type);
394 
395  mp_integer max_bytes=0;
396  exprt result=from_integer(0, size_type());
397 
398  // compute max
399 
400  for(const auto &c : union_type.components())
401  {
402  const typet &subtype = c.type();
403  exprt sub_size;
404 
405  auto sub_bits = pointer_offset_bits(subtype, ns);
406 
407  if(!sub_bits.has_value())
408  {
409  max_bytes=-1;
410 
411  auto sub_size_opt = size_of_expr(subtype, ns);
412  if(!sub_size_opt.has_value())
413  return {};
414  sub_size = sub_size_opt.value();
415  }
416  else
417  {
418  mp_integer sub_bytes = (*sub_bits + 7) / 8;
419 
420  if(max_bytes>=0)
421  {
422  if(max_bytes<sub_bytes)
423  {
424  max_bytes=sub_bytes;
425  result=from_integer(sub_bytes, size_type());
426  }
427 
428  continue;
429  }
430 
431  sub_size=from_integer(sub_bytes, size_type());
432  }
433 
434  result=if_exprt(
435  binary_relation_exprt(result, ID_lt, sub_size),
436  sub_size, result);
437 
438  simplify(result, ns);
439  }
440 
441  return result;
442  }
443  else if(type.id()==ID_signedbv ||
444  type.id()==ID_unsignedbv ||
445  type.id()==ID_fixedbv ||
446  type.id()==ID_floatbv ||
447  type.id()==ID_bv ||
448  type.id()==ID_c_bool ||
449  type.id()==ID_c_bit_field)
450  {
451  std::size_t width=to_bitvector_type(type).get_width();
452  std::size_t bytes=width/8;
453  if(bytes*8!=width)
454  bytes++;
455  return from_integer(bytes, size_type());
456  }
457  else if(type.id()==ID_c_enum)
458  {
459  std::size_t width =
460  to_bitvector_type(to_c_enum_type(type).subtype()).get_width();
461  std::size_t bytes=width/8;
462  if(bytes*8!=width)
463  bytes++;
464  return from_integer(bytes, size_type());
465  }
466  else if(type.id()==ID_c_enum_tag)
467  {
468  return size_of_expr(ns.follow_tag(to_c_enum_tag_type(type)), ns);
469  }
470  else if(type.id()==ID_bool)
471  {
472  return from_integer(1, size_type());
473  }
474  else if(type.id()==ID_pointer)
475  {
476  // the following is an MS extension
477  if(type.get_bool(ID_C_ptr32))
478  return from_integer(4, size_type());
479 
480  std::size_t width=to_bitvector_type(type).get_width();
481  std::size_t bytes=width/8;
482  if(bytes*8!=width)
483  bytes++;
484  return from_integer(bytes, size_type());
485  }
486  else if(type.id() == ID_union_tag)
487  {
488  return size_of_expr(ns.follow_tag(to_union_tag_type(type)), ns);
489  }
490  else if(type.id() == ID_struct_tag)
491  {
492  return size_of_expr(ns.follow_tag(to_struct_tag_type(type)), ns);
493  }
494  else if(type.id()==ID_code)
495  {
496  return from_integer(0, size_type());
497  }
498  else if(type.id()==ID_string)
499  {
500  return from_integer(32/8, size_type());
501  }
502  else
503  return {};
504 }
505 
507 compute_pointer_offset(const exprt &expr, const namespacet &ns)
508 {
509  if(expr.id()==ID_symbol)
510  {
511  if(is_ssa_expr(expr))
512  return compute_pointer_offset(
513  to_ssa_expr(expr).get_original_expr(), ns);
514  else
515  return mp_integer(0);
516  }
517  else if(expr.id()==ID_index)
518  {
519  const index_exprt &index_expr=to_index_expr(expr);
521  index_expr.array().type().id() == ID_array,
522  "index into array expected, found " +
523  index_expr.array().type().id_string());
524 
525  auto o = compute_pointer_offset(index_expr.array(), ns);
526 
527  if(o.has_value())
528  {
529  const auto &array_type = to_array_type(index_expr.array().type());
530  auto sub_size = pointer_offset_size(array_type.subtype(), ns);
531 
532  if(sub_size.has_value() && *sub_size > 0)
533  {
534  const auto i = numeric_cast<mp_integer>(index_expr.index());
535  if(i.has_value())
536  return (*o) + (*i) * (*sub_size);
537  }
538  }
539 
540  // don't know
541  }
542  else if(expr.id()==ID_member)
543  {
544  const member_exprt &member_expr=to_member_expr(expr);
545  const exprt &op=member_expr.struct_op();
546  const struct_union_typet &type=to_struct_union_type(ns.follow(op.type()));
547 
548  auto o = compute_pointer_offset(op, ns);
549 
550  if(o.has_value())
551  {
552  if(type.id()==ID_union)
553  return *o;
554 
556  to_struct_type(type), member_expr.get_component_name(), ns);
557 
558  if(member_offset.has_value())
559  return *o + *member_offset;
560  }
561  }
562  else if(expr.id()==ID_string_constant)
563  return mp_integer(0);
564 
565  return {}; // don't know
566 }
567 
570 {
571  const typet &type=
572  static_cast<const typet &>(expr.find(ID_C_c_sizeof_type));
573 
574  if(type.is_nil())
575  return {};
576 
577  const auto type_size = pointer_offset_size(type, ns);
578  auto val = numeric_cast<mp_integer>(expr);
579 
580  if(
581  !type_size.has_value() || *type_size < 0 || !val.has_value() ||
582  *val < *type_size || (*type_size == 0 && *val > 0))
583  {
584  return {};
585  }
586 
587  const typet t(size_type());
589  address_bits(*val + 1) <= *pointer_offset_bits(t, ns),
590  "sizeof value does not fit size_type");
591 
592  mp_integer remainder=0;
593 
594  if(*type_size != 0)
595  {
596  remainder = *val % *type_size;
597  *val -= remainder;
598  *val /= *type_size;
599  }
600 
601  exprt result(ID_sizeof, t);
602  result.set(ID_type_arg, type);
603 
604  if(*val > 1)
605  result = mult_exprt(result, from_integer(*val, t));
606  if(remainder>0)
607  result=plus_exprt(result, from_integer(remainder, t));
608 
609  return typecast_exprt::conditional_cast(result, expr.type());
610 }
611 
613  const exprt &expr,
614  const mp_integer &offset_bytes,
615  const typet &target_type_raw,
616  const namespacet &ns)
617 {
618  if(offset_bytes == 0 && expr.type() == target_type_raw)
619  {
620  exprt result = expr;
621 
622  if(expr.type() != target_type_raw)
623  result.type() = target_type_raw;
624 
625  return result;
626  }
627 
628  if(
629  offset_bytes == 0 && expr.type().id() == ID_pointer &&
630  target_type_raw.id() == ID_pointer)
631  {
632  return typecast_exprt(expr, target_type_raw);
633  }
634 
635  const typet &source_type = ns.follow(expr.type());
636  const auto target_size_bits = pointer_offset_bits(target_type_raw, ns);
637  if(!target_size_bits.has_value())
638  return {};
639 
640  if(source_type.id()==ID_struct)
641  {
642  const struct_typet &struct_type = to_struct_type(source_type);
643 
644  mp_integer m_offset_bits = 0;
645  for(const auto &component : struct_type.components())
646  {
647  const auto m_size_bits = pointer_offset_bits(component.type(), ns);
648  if(!m_size_bits.has_value())
649  return {};
650 
651  // if this member completely contains the target, and this member is
652  // byte-aligned, recurse into it
653  if(
654  offset_bytes * 8 >= m_offset_bits && m_offset_bits % 8 == 0 &&
655  offset_bytes * 8 + *target_size_bits <= m_offset_bits + *m_size_bits)
656  {
657  const member_exprt member(expr, component.get_name(), component.type());
659  member, offset_bytes - m_offset_bits / 8, target_type_raw, ns);
660  }
661 
662  m_offset_bits += *m_size_bits;
663  }
664  }
665  else if(source_type.id()==ID_array)
666  {
667  const array_typet &array_type = to_array_type(source_type);
668 
669  const auto elem_size_bits = pointer_offset_bits(array_type.subtype(), ns);
670 
671  // no arrays of non-byte-aligned, zero-, or unknown-sized objects
672  if(
673  !elem_size_bits.has_value() || *elem_size_bits == 0 ||
674  *elem_size_bits % 8 != 0)
675  {
676  return {};
677  }
678 
679  if(*target_size_bits <= *elem_size_bits)
680  {
681  const mp_integer elem_size_bytes = *elem_size_bits / 8;
682  const auto offset_inside_elem = offset_bytes % elem_size_bytes;
683  const auto target_size_bytes = *target_size_bits / 8;
684  // only recurse if the cell completely contains the target
685  if(offset_inside_elem + target_size_bytes <= elem_size_bytes)
686  {
688  index_exprt(
689  expr, from_integer(offset_bytes / elem_size_bytes, index_type())),
690  offset_inside_elem,
691  target_type_raw,
692  ns);
693  }
694  }
695  }
696 
697  return byte_extract_exprt(
698  byte_extract_id(),
699  expr,
700  from_integer(offset_bytes, index_type()),
701  target_type_raw);
702 }
703 
705  const exprt &expr,
706  const exprt &offset,
707  const typet &target_type,
708  const namespacet &ns)
709 {
710  const auto offset_bytes = numeric_cast<mp_integer>(offset);
711 
712  if(!offset_bytes.has_value())
713  return {};
714  else
715  return get_subexpression_at_offset(expr, *offset_bytes, target_type, ns);
716 }
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:142
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:555
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_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:721
typecast_exprt::conditional_cast
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:2021
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:303
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:209
exprt::size
std::size_t size() const
Amount of nodes this expression tree contains.
Definition: expr.cpp:26
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
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:681
typet
The type of an expression, extends irept.
Definition: type.h:29
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1347
struct_union_typet
Base type for structs and unions.
Definition: std_types.h:57
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:2964
irept::find
const irept & find(const irep_namet &name) const
Definition: irep.cpp:103
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:881
exprt
Base class for all expressions.
Definition: expr.h:53
struct_union_typet::componentst
std::vector< componentt > componentst
Definition: std_types.h:135
namespace_baset::follow_tag
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:65
component
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:192
to_complex_type
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
Definition: std_types.h:1815
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:176
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:507
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:81
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:128
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:148
member_exprt::struct_op
const exprt & struct_op() const
Definition: std_expr.h:3435
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
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:1471
irept::id_string
const std::string & id_string() const
Definition: irep.h:421
simplify
bool simplify(exprt &expr, const namespacet &ns)
Definition: simplify_expr.cpp:2693
mult_exprt
Binary multiplication Associativity is not specified.
Definition: std_expr.h:986
simplify_expr
exprt simplify_expr(exprt src, const namespacet &ns)
Definition: simplify_expr.cpp:2698
index_exprt::index
exprt & index()
Definition: std_expr.h:1319
index_exprt::array
exprt & array()
Definition: std_expr.h:1309
irept::is_nil
bool is_nil() const
Definition: irep.h:398
irept::id
const irep_idt & id() const
Definition: irep.h:418
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:515
union_typet
The union type.
Definition: std_types.h:393
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
vector_typet::size
const constant_exprt & size() const
Definition: std_types.cpp:268
simplify_expr.h
bitvector_typet::get_width
std::size_t get_width() const
Definition: std_types.h:1041
member_exprt
Extract member of struct or union.
Definition: std_expr.h:3405
ssa_expr.h
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:226
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:965
build_sizeof_expr
optionalt< exprt > build_sizeof_expr(const constant_exprt &expr, const namespacet &ns)
Definition: pointer_offset_size.cpp:569
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:51
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:442
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
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:612
binary_relation_exprt
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:725
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:1011
to_vector_type
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition: std_types.h:1775
size_of_expr
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
Definition: pointer_offset_size.cpp:285
to_member_expr
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:3489
member_exprt::get_component_name
irep_idt get_component_name() const
Definition: std_expr.h:3419
to_union_type
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition: std_types.h:422
index_exprt
Array index operator.
Definition: std_expr.h:1293
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:2013
size_type
unsignedbv_typet size_type()
Definition: c_types.cpp:58
constant_exprt
A constant literal expression.
Definition: std_expr.h:3906
member_offset_expr
optionalt< exprt > member_offset_expr(const member_exprt &member_expr, const namespacet &ns)
Definition: pointer_offset_size.cpp:226
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
to_bitvector_type
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
Definition: std_types.h:1089