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