CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
value_set_dereference.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Symbolic Execution of ANSI-C
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
13
14#ifdef DEBUG
15#include <iostream>
16#endif
17
18#include <util/arith_tools.h>
19#include <util/byte_operators.h>
20#include <util/c_types.h>
21#include <util/config.h>
22#include <util/cprover_prefix.h>
23#include <util/expr_iterator.h>
24#include <util/expr_util.h>
25#include <util/format_expr.h>
26#include <util/fresh_symbol.h>
27#include <util/json.h>
28#include <util/message.h>
29#include <util/namespace.h>
30#include <util/pointer_expr.h>
33#include <util/range.h>
34#include <util/simplify_expr.h>
35#include <util/symbol.h>
36
38
39#include <deque>
40
51static bool should_use_local_definition_for(const exprt &expr)
52{
53 bool seen_symbol = false;
54 for(auto it = expr.depth_begin(), itend = expr.depth_end(); it != itend; ++it)
55 {
56 if(it->id() == ID_symbol)
57 {
58 if(seen_symbol)
59 return true;
60 else
61 seen_symbol = true;
62 }
63 }
64
65 return false;
66}
67
69 const exprt &pointer,
70 const std::vector<exprt> &points_to_set,
71 const std::vector<exprt> &retained_values,
72 const exprt &value)
73{
75 json_result["Pointer"] = json_stringt{format_to_string(pointer)};
76 json_result["PointsToSetSize"] =
77 json_numbert{std::to_string(points_to_set.size())};
78
80 for(const auto &object : points_to_set)
81 {
83 }
84
85 json_result["PointsToSet"] = points_to_set_json;
86
87 json_result["RetainedValuesSetSize"] =
88 json_numbert{std::to_string(points_to_set.size())};
89
92 {
95 }
96
97 json_result["RetainedValuesSet"] = retained_values_set_json;
98
99 json_result["Value"] = json_stringt{format_to_string(value)};
100
101 return json_result;
102}
103
107static std::optional<exprt>
109{
110 if(const auto *index_expr = expr_try_dynamic_cast<index_exprt>(expr))
111 {
112 return index_exprt{
113 index_expr->array(),
114 plus_exprt{index_expr->index(),
116 offset_elements, index_expr->index().type())}};
117 }
118 else if(const auto *if_expr = expr_try_dynamic_cast<if_exprt>(expr))
119 {
120 const auto true_case =
122 if(!true_case)
123 return {};
124 const auto false_case =
126 if(!false_case)
127 return {};
128 return if_exprt{if_expr->cond(), *true_case, *false_case};
129 }
130 else if(can_cast_expr<typecast_exprt>(expr))
131 {
132 // the case of a type cast is _not_ handled here, because that would require
133 // doing arithmetic on the offset, and may result in an offset into some
134 // sub-element
135 return {};
136 }
137 else
138 {
139 return {};
140 }
141}
142
144 const exprt &pointer,
146{
148 pointer.type().id() == ID_pointer,
149 "dereference expected pointer type, but got " + pointer.type().pretty());
150
151 // we may get ifs due to recursive calls
152 if(pointer.id()==ID_if)
153 {
154 const if_exprt &if_expr=to_if_expr(pointer);
155 exprt true_case = dereference(if_expr.true_case(), display_points_to_sets);
156 exprt false_case =
158 return if_exprt(if_expr.cond(), true_case, false_case);
159 }
160 else if(pointer.id() == ID_typecast)
161 {
162 const exprt *underlying = &pointer;
163 // Note this isn't quite the same as skip_typecast, which would also skip
164 // things such as int-to-ptr typecasts which we shouldn't ignore
165 while(underlying->id() == ID_typecast &&
166 underlying->type().id() == ID_pointer)
167 {
168 underlying = &to_typecast_expr(*underlying).op();
169 }
170
171 if(underlying->id() == ID_if && underlying->type().id() == ID_pointer)
172 {
173 const auto &if_expr = to_if_expr(*underlying);
174 return if_exprt(
175 if_expr.cond(),
177 typecast_exprt(if_expr.true_case(), pointer.type()),
180 typecast_exprt(if_expr.false_case(), pointer.type()),
182 }
183 }
184 else if(pointer.id() == ID_plus && pointer.operands().size() == 2)
185 {
186 // Try to improve results for *(p + i) where p points to known offsets but
187 // i is non-constant-- if `p` points to known positions in arrays or array-members
188 // of structs then we can add the non-constant expression `i` to the index
189 // instead of using a byte-extract expression.
190
191 exprt pointer_expr = to_plus_expr(pointer).op0();
192 exprt offset_expr = to_plus_expr(pointer).op1();
193
195 std::swap(pointer_expr, offset_expr);
196
197 if(
198 can_cast_type<pointer_typet>(pointer_expr.type()) &&
199 pointer_expr.id() != ID_typecast &&
202 {
203 exprt derefd_pointer = dereference(pointer_expr);
204 if(
205 auto derefd_with_offset =
207 return *derefd_with_offset;
208
209 // If any of this fails, fall through to use the normal byte-extract path.
210 }
211 }
212
214}
215
217 const exprt &pointer,
219{ // type of the object
220 const typet &type = to_pointer_type(pointer.type()).base_type();
221
222 // collect objects the pointer may point to
223 const std::vector<exprt> points_to_set =
225
226 // get the values of these
227 const std::vector<exprt> retained_values =
228 make_range(points_to_set).filter([&](const exprt &value) {
230 });
231
233
234 if(retained_values.size() >= 2 && should_use_local_definition_for(pointer))
235 {
237 pointer.type(),
238 "derefd_pointer",
239 "derefd_pointer",
240 pointer.find_source_location(),
243
245 }
246
247 auto values =
249 .map([&](const exprt &value) {
251 })
252 .collect<std::deque<valuet>>();
253
254 const bool may_fail =
255 values.empty() ||
256 std::any_of(values.begin(), values.end(), [](const valuet &value) {
257 return value.value.is_nil();
258 });
259
260 if(may_fail)
261 {
262 values.push_front(get_failure_value(pointer, type));
263 }
264
265 // now build big case split, but we only do "good" objects
266
267 exprt result_value = nil_exprt{};
268
269 for(const auto &value : values)
270 {
271 if(value.value.is_not_nil())
272 {
273 if(result_value.is_nil()) // first?
274 result_value = value.value;
275 else
276 result_value = if_exprt(value.pointer_guard, value.value, result_value);
277 }
278 }
279
280 if(compare_against_pointer != pointer)
281 result_value =
282 let_exprt(to_symbol_expr(compare_against_pointer), pointer, result_value);
283
285 {
288 pointer, points_to_set, retained_values, result_value);
289 }
290
291 return result_value;
292}
293
295 const exprt &pointer,
296 const typet &type)
297{
298 // first see if we have a "failed object" for this pointer
300
301 if(
302 const symbolt *failed_symbol =
304 {
305 // yes!
306 failure_value = failed_symbol->symbol_expr();
308 }
309 else
310 {
311 // else: produce new symbol
313 type,
314 "symex",
315 "invalid_object",
316 pointer.source_location(),
319
320 // make it a lvalue, so we can assign to it
321 symbol.is_lvalue = true;
322
323 failure_value = symbol.symbol_expr();
325 }
326
327 valuet result{};
328 result.value = failure_value;
329 result.pointer_guard = true_exprt();
330 return result;
331}
332
342 const typet &object_type,
343 const typet &dereference_type,
344 const namespacet &ns)
345{
346 const typet *object_unwrapped = &object_type;
348 while(object_unwrapped->id() == ID_pointer &&
350 {
351 object_unwrapped = &to_pointer_type(*object_unwrapped).base_type();
353 &to_pointer_type(*dereference_unwrapped).base_type();
354 }
356 {
357 return true;
358 }
359 else if(dereference_unwrapped->id() == ID_pointer &&
361 {
362#ifdef DEBUG
363 std::cout << "value_set_dereference: the dereference type has "
364 "too many ID_pointer levels"
365 << std::endl;
366 std::cout << " object_type: " << object_type.pretty() << std::endl;
367 std::cout << " dereference_type: " << dereference_type.pretty()
368 << std::endl;
369#endif
370 }
371
372 if(object_type == dereference_type)
373 return true; // ok, they just match
374
375 // check for struct prefixes
376 const typet &ot_base = object_type.id() == ID_struct_tag
377 ? ns.follow_tag(to_struct_tag_type(object_type))
378 : object_type;
382
383 if(ot_base.id()==ID_struct &&
384 dt_base.id()==ID_struct)
385 {
386 if(to_struct_type(dt_base).is_prefix_of(
388 return true; // ok, dt is a prefix of ot
389 }
390
391 // we are generous about code pointers
392 if(dereference_type.id()==ID_code &&
393 object_type.id()==ID_code)
394 return true;
395
396 // bitvectors of same width are ok
397 if((dereference_type.id()==ID_signedbv ||
399 (object_type.id()==ID_signedbv ||
400 object_type.id()==ID_unsignedbv) &&
402 to_bitvector_type(object_type).get_width())
403 return true;
404
405 // really different
406
407 return false;
408}
409
424 const exprt &what,
425 bool exclude_null_derefs,
426 const irep_idt &language_mode)
427{
428 if(what.id() == ID_unknown || what.id() == ID_invalid)
429 {
430 return false;
431 }
432
434
435 const exprt &root_object = o.root_object();
436 if(root_object.id() == ID_null_object)
437 {
438 return exclude_null_derefs;
439 }
440 else if(root_object.id() == ID_integer_address)
441 {
442 return language_mode == ID_java;
443 }
444
445 return false;
446}
447
461 const exprt &what,
462 const exprt &pointer_expr,
463 const namespacet &ns)
464{
468
469 if(what.id()==ID_unknown ||
470 what.id()==ID_invalid)
471 {
472 return valuet();
473 }
474
476 what.id() == ID_object_descriptor,
477 "unknown points-to: " + what.id_string());
478
480
481 const exprt &root_object=o.root_object();
482 const exprt &object=o.object();
483
484 #if 0
485 std::cout << "O: " << format(root_object) << '\n';
486 #endif
487
488 if(root_object.id() == ID_null_object)
489 {
490 if(!o.offset().is_zero())
491 return {};
492
493 valuet result;
495 return result;
496 }
497 else if(root_object.id()==ID_dynamic_object)
498 {
499 valuet result;
500
501 // constraint that it actually is a dynamic object
502 // this is also our guard
503 result.pointer_guard = is_dynamic_object_exprt(pointer_expr);
504
505 // can't remove here, turn into *p
506 result.value = dereference_exprt{pointer_expr};
507 result.pointer = pointer_expr;
508
509 return result;
510 }
511 else if(root_object.id()==ID_integer_address)
512 {
513 // This is stuff like *((char *)5).
514 // This is turned into an access to __CPROVER_memory[...].
515
516 const symbolt &memory_symbol=ns.lookup(CPROVER_PREFIX "memory");
517 const symbol_exprt symbol_expr(memory_symbol.name, memory_symbol.type);
518
519 if(to_array_type(memory_symbol.type).element_type() == dereference_type)
520 {
521 // Types match already, what a coincidence!
522 // We can use an index expression.
523
525 symbol_expr,
527 pointer_offset(pointer_expr),
528 to_array_type(memory_symbol.type).index_type()),
529 to_array_type(memory_symbol.type).element_type());
530
531 valuet result;
532 result.value=index_expr;
534 return result;
535 }
537 to_array_type(memory_symbol.type).element_type(),
539 ns))
540 {
542 symbol_expr,
544 pointer_offset(pointer_expr),
545 to_array_type(memory_symbol.type).index_type()),
546 to_array_type(memory_symbol.type).element_type());
547
548 valuet result;
550 result.pointer =
552 return result;
553 }
554 else
555 {
556 // We need to use byte_extract.
557 // Won't do this without a commitment to an endianness.
558
560 return {};
561
562 valuet result;
563 result.value = make_byte_extract(
564 symbol_expr, pointer_offset(pointer_expr), dereference_type);
565 result.pointer = address_of_exprt{result.value};
566 return result;
567 }
568 }
569 else
570 {
571 valuet result;
572
573 // something generic -- really has to be a symbol
575
576 if(o.offset().is_zero())
577 {
578 result.pointer_guard = equal_exprt(
581 }
582 else
583 {
584 result.pointer_guard=same_object(pointer_expr, object_pointer);
585 }
586
587 const typet &object_type = object.type();
588 const typet &root_object_type = root_object.type();
589
590 if(
592 o.offset().is_zero())
593 {
594 // The simplest case: types match, and offset is zero!
595 // This is great, we are almost done.
596
598 result.pointer =
600
601 return result;
602 }
603
604 // this is relative to the root object
605 exprt offset;
606 if(o.offset().is_constant())
607 offset = o.offset();
608 else
609 offset = simplify_expr(pointer_offset(pointer_expr), ns);
610
611 if(
612 root_object_type.id() == ID_array &&
617 offset.is_constant())
618 {
619 // We have an array with a subtype that matches
620 // the dereferencing type.
621
622 // are we doing a byte?
623 auto element_size =
625 CHECK_RETURN(element_size.has_value());
627
628 const auto offset_int =
630
631 if(offset_int % *element_size == 0)
632 {
634 root_object,
637 to_array_type(root_object_type).index_type())};
638 result.value =
642
643 return result;
644 }
645 }
646
647 // try to build a member/index expression - do not use byte_extract
649 root_object, o.offset(), dereference_type, ns);
650 if(subexpr.has_value())
651 simplify(subexpr.value(), ns);
652 if(
653 subexpr.has_value() &&
654 subexpr.value().id() != ID_byte_extract_little_endian &&
655 subexpr.value().id() != ID_byte_extract_big_endian)
656 {
657 // Successfully found a member, array index, or combination thereof
658 // that matches the desired type and offset:
659 result.value = subexpr.value();
662 return result;
663 }
664
665 // we extract something from the root object
666 result.value = o.root_object();
669
670 if(memory_model(result.value, dereference_type, offset, ns))
671 {
672 // set pointer correctly
676 result.pointer,
678 offset),
680 }
681 else
682 {
683 return {}; // give up, no way that this is ok
684 }
685
686 return result;
687 }
688}
689
690static bool is_a_bv_type(const typet &type)
691{
692 return type.id()==ID_unsignedbv ||
693 type.id()==ID_signedbv ||
694 type.id()==ID_bv ||
695 type.id()==ID_fixedbv ||
696 type.id()==ID_floatbv ||
697 type.id()==ID_c_enum_tag;
698}
699
709 exprt &value,
710 const typet &to_type,
711 const exprt &offset,
712 const namespacet &ns)
713{
714 // we will allow more or less arbitrary pointer type cast
715
716 const typet from_type=value.type();
717
718 // first, check if it's really just a type coercion,
719 // i.e., both have exactly the same (constant) size,
720 // for bit-vector types or pointers
721
722 if(
723 (is_a_bv_type(from_type) && is_a_bv_type(to_type)) ||
724 (from_type.id() == ID_pointer && to_type.id() == ID_pointer))
725 {
727 {
728 // avoid semantic conversion in case of
729 // cast to float or fixed-point,
730 // or cast from float or fixed-point
731
732 if(
733 to_type.id() != ID_fixedbv && to_type.id() != ID_floatbv &&
734 from_type.id() != ID_fixedbv && from_type.id() != ID_floatbv)
735 {
736 value = typecast_exprt::conditional_cast(value, to_type);
737 return true;
738 }
739 }
740 }
741
742 // otherwise, we will stitch it together from bytes
743
744 return memory_model_bytes(value, to_type, offset, ns);
745}
746
756 exprt &value,
757 const typet &to_type,
758 const exprt &offset,
759 const namespacet &ns)
760{
761 const typet from_type=value.type();
762
763 // We simply refuse to convert to/from code.
764 if(from_type.id()==ID_code || to_type.id()==ID_code)
765 return false;
766
767 // We won't do this without a commitment to an endianness.
769 return false;
770
771 // But everything else we will try!
772 // We just rely on byte_extract to do the job!
773
774 exprt result;
775
776 // See if we have an array of bytes already,
777 // and we want something byte-sized.
779 from_type.id() == ID_array
781 : std::optional<mp_integer>{};
782
783 auto to_type_size = pointer_offset_size(to_type, ns);
784
785 if(
786 from_type.id() == ID_array && from_type_element_type_size.has_value() &&
787 *from_type_element_type_size == 1 && to_type_size.has_value() &&
788 *to_type_size == 1 &&
789 is_a_bv_type(to_array_type(from_type).element_type()) &&
790 is_a_bv_type(to_type))
791 {
792 // yes, can use 'index', but possibly need to convert
795 value,
797 offset, to_array_type(from_type).index_type()),
798 to_array_type(from_type).element_type()),
799 to_type);
800 }
801 else
802 {
803 // no, use 'byte_extract'
804 result = make_byte_extract(value, offset, to_type);
805 }
806
807 value=result;
808
809 return true;
810}
configt config
Definition config.cpp:25
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
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.
pointer_typet pointer_type(const typet &subtype)
Definition c_types.cpp:235
bitvector_typet char_type()
Definition c_types.cpp:106
Operator to return the address of an object.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
std::size_t get_width() const
Definition std_types.h:925
struct configt::ansi_ct ansi_c
virtual const symbolt * get_or_create_failed_symbol(const exprt &expr)=0
virtual std::vector< exprt > get_value_set(const exprt &expr) const =0
Operator to dereference a pointer.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
Equality.
Definition std_expr.h:1366
Base class for all expressions.
Definition expr.h:56
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
Definition expr.cpp:147
depth_iteratort depth_end()
Definition expr.cpp:249
depth_iteratort depth_begin()
Definition expr.cpp:247
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition expr.cpp:47
bool is_constant() const
Return whether the expression is a constant.
Definition expr.h:212
typet & type()
Return the type of the expression.
Definition expr.h:84
operandst & operands()
Definition expr.h:94
const source_locationt & source_location() const
Definition expr.h:231
The trinary if-then-else operator.
Definition std_expr.h:2497
Array index operator.
Definition std_expr.h:1470
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition irep.cpp:482
bool is_not_nil() const
Definition irep.h:372
const std::string & id_string() const
Definition irep.h:391
const irep_idt & id() const
Definition irep.h:388
bool is_nil() const
Definition irep.h:368
Evaluates to true if the operand is a pointer to a dynamic object.
A let expression.
Definition std_expr.h:3331
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:154
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
The NIL expression.
Definition std_expr.h:3208
The null pointer constant.
Split an expression into a base object and a (byte) offset.
static const exprt & root_object(const exprt &expr)
The plus expression Associativity is not specified.
Definition std_expr.h:1002
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
const typet & base_type() const
The type of the data what we point to.
Expression to hold a symbol (variable)
Definition std_expr.h:131
Symbol table entry.
Definition symbol.h:28
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition symbol.cpp:121
bool is_lvalue
Definition symbol.h:72
The Boolean constant true.
Definition std_expr.h:3190
Semantic type conversion.
Definition std_expr.h:2073
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:2081
The type of an expression, extends irept.
Definition type.h:29
Return value for build_reference_to; see that method for documentation.
static bool memory_model_bytes(exprt &value, const typet &type, const exprt &offset, const namespacet &ns)
Replace value by an expression of type to_type corresponding to the value at memory address value + o...
valuet get_failure_value(const exprt &pointer, const typet &type)
exprt handle_dereference_base_case(const exprt &pointer, bool display_points_to_sets)
const bool exclude_null_derefs
Flag indicating whether value_set_dereferencet::dereference should disregard an apparent attempt to d...
symbol_table_baset & new_symbol_table
static bool dereference_type_compare(const typet &object_type, const typet &dereference_type, const namespacet &ns)
Check if the two types have matching number of ID_pointer levels, with the dereference type eventuall...
message_handlert & message_handler
dereference_callbackt & dereference_callback
exprt dereference(const exprt &pointer, bool display_points_to_sets=false)
Dereference the given pointer-expression.
const irep_idt language_mode
language_mode: ID_java, ID_C or another language identifier if we know the source language in use,...
static valuet build_reference_to(const exprt &what, const exprt &pointer, const namespacet &ns)
static bool should_ignore_value(const exprt &what, bool exclude_null_derefs, const irep_idt &language_mode)
Determine whether possible alias what should be ignored when replacing a pointer by its referees.
static bool memory_model(exprt &value, const typet &type, const exprt &offset, const namespacet &ns)
Replace value by an expression of type to_type corresponding to the value at memory address value + o...
#define CPROVER_PREFIX
Pointer Dereferencing.
Forward depth-first search iterators These iterators' copy operations are expensive,...
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
Deprecated expression utility functions.
static format_containert< T > format(const T &o)
Definition format.h:37
std::string format_to_string(const T &o)
Definition format.h:43
symbolt & get_fresh_aux_symbol(const typet &type, const std::string &name_prefix, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &symbol_mode, const namespacet &ns, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with respect to the given namespace ns with the requested name pattern ...
Fresh auxiliary symbol creation.
std::string from_type(const namespacet &ns, const irep_idt &identifier, const typet &type)
double log(double x)
Definition math.c:2449
API to expression classes for Pointers.
const object_descriptor_exprt & to_object_descriptor_expr(const exprt &expr)
Cast an exprt to an object_descriptor_exprt.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
std::optional< mp_integer > pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
std::optional< exprt > get_subexpression_at_offset(const exprt &expr, const mp_integer &offset_bytes, const typet &target_type_raw, const namespacet &ns)
std::optional< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
Pointer Logic.
exprt pointer_offset(const exprt &pointer)
exprt same_object(const exprt &p1, const exprt &p2)
Various predicates over pointers in programs.
Ranges: pair of begin and end iterators, which can be initialized from containers,...
ranget< iteratort > make_range(iteratort begin, iteratort end)
Definition range.h:522
bool simplify(exprt &expr, const namespacet &ns)
exprt simplify_expr(exprt src, const namespacet &ns)
#define PRECONDITION_WITH_DIAGNOSTICS(CONDITION,...)
Definition invariant.h:464
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition std_expr.h:2107
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
Definition std_expr.h:1041
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition std_expr.h:2577
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition std_expr.h:3172
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:272
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:518
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:888
Symbol table entry.
static std::optional< exprt > try_add_offset_to_indices(const exprt &expr, const exprt &offset_elements)
If expr is of the form (c1 ? e1[o1] : c2 ? e2[o2] : c3 ? ...) then return c1 ? e1[o1 + offset] : e2[o...
static bool is_a_bv_type(const typet &type)
static json_objectt value_set_dereference_stats_to_json(const exprt &pointer, const std::vector< exprt > &points_to_set, const std::vector< exprt > &retained_values, const exprt &value)
static bool should_use_local_definition_for(const exprt &expr)
Returns true if expr is complicated enough that a local definition (using a let expression) is prefer...
Pointer Dereferencing.