cprover
value_set_dereference.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Symbolic Execution of ANSI-C
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "value_set_dereference.h"
13 
14 #ifdef DEBUG
15 #include <iostream>
16 #include <util/format_expr.h>
17 #endif
18 
19 #include <util/arith_tools.h>
20 #include <util/array_name.h>
21 #include <util/byte_operators.h>
22 #include <util/c_types.h>
23 #include <util/config.h>
24 #include <util/cprover_prefix.h>
25 #include <util/expr_iterator.h>
26 #include <util/expr_util.h>
27 #include <util/format_type.h>
28 #include <util/fresh_symbol.h>
29 #include <util/options.h>
32 #include <util/range.h>
33 #include <util/simplify_expr.h>
34 #include <util/ssa_expr.h>
35 
46 static bool should_use_local_definition_for(const exprt &expr)
47 {
48  bool seen_symbol = false;
49  for(auto it = expr.depth_begin(), itend = expr.depth_end(); it != itend; ++it)
50  {
51  if(it->id() == ID_symbol)
52  {
53  if(seen_symbol)
54  return true;
55  else
56  seen_symbol = true;
57  }
58  }
59 
60  return false;
61 }
62 
64 {
65  if(pointer.type().id()!=ID_pointer)
66  throw "dereference expected pointer type, but got "+
67  pointer.type().pretty();
68 
69  // we may get ifs due to recursive calls
70  if(pointer.id()==ID_if)
71  {
72  const if_exprt &if_expr=to_if_expr(pointer);
73  exprt true_case = dereference(if_expr.true_case());
74  exprt false_case = dereference(if_expr.false_case());
75  return if_exprt(if_expr.cond(), true_case, false_case);
76  }
77  else if(pointer.id() == ID_typecast)
78  {
79  const exprt *underlying = &pointer;
80  // Note this isn't quite the same as skip_typecast, which would also skip
81  // things such as int-to-ptr typecasts which we shouldn't ignore
82  while(underlying->id() == ID_typecast &&
83  underlying->type().id() == ID_pointer)
84  {
85  underlying = &to_typecast_expr(*underlying).op();
86  }
87 
88  if(underlying->id() == ID_if && underlying->type().id() == ID_pointer)
89  {
90  const auto &if_expr = to_if_expr(*underlying);
91  return if_exprt(
92  if_expr.cond(),
93  dereference(typecast_exprt(if_expr.true_case(), pointer.type())),
94  dereference(typecast_exprt(if_expr.false_case(), pointer.type())));
95  }
96  }
97 
98  // type of the object
99  const typet &type=pointer.type().subtype();
100 
101 #ifdef DEBUG
102  std::cout << "value_set_dereferencet::dereference pointer=" << format(pointer)
103  << '\n';
104 #endif
105 
106  // collect objects the pointer may point to
107  const std::vector<exprt> points_to_set =
109 
110 #ifdef DEBUG
111  std::cout << "value_set_dereferencet::dereference points_to_set={";
112  for(auto p : points_to_set)
113  std::cout << format(p) << "; ";
114  std::cout << "}\n" << std::flush;
115 #endif
116 
117  // get the values of these
118  const std::vector<exprt> retained_values =
119  make_range(points_to_set).filter([&](const exprt &value) {
121  });
122 
123  exprt compare_against_pointer = pointer;
124 
125  if(retained_values.size() >= 2 && should_use_local_definition_for(pointer))
126  {
127  symbolt fresh_binder = get_fresh_aux_symbol(
128  pointer.type(),
129  "derefd_pointer",
130  "derefd_pointer",
134 
135  compare_against_pointer = fresh_binder.symbol_expr();
136  }
137 
138 #ifdef DEBUG
139  std::cout << "value_set_dereferencet::dereference retained_values={";
140  for(const auto &value : retained_values)
141  std::cout << format(value) << "; ";
142  std::cout << "}\n" << std::flush;
143 #endif
144 
145  std::list<valuet> values =
146  make_range(retained_values).map([&](const exprt &value) {
147  return build_reference_to(value, compare_against_pointer, ns);
148  });
149 
150  // can this fail?
151  bool may_fail;
152 
153  if(values.empty())
154  {
155  may_fail=true;
156  }
157  else
158  {
159  may_fail=false;
160  for(std::list<valuet>::const_iterator
161  it=values.begin();
162  it!=values.end();
163  it++)
164  if(it->value.is_nil())
165  may_fail=true;
166  }
167 
168  if(may_fail)
169  {
170  // first see if we have a "failed object" for this pointer
171 
172  exprt failure_value;
173 
174  if(
175  const symbolt *failed_symbol =
177  {
178  // yes!
179  failure_value=failed_symbol->symbol_expr();
180  failure_value.set(ID_C_invalid_object, true);
181  }
182  else
183  {
184  // else: produce new symbol
185  symbolt &symbol = get_fresh_aux_symbol(
186  type,
187  "symex",
188  "invalid_object",
189  pointer.source_location(),
192 
193  // make it a lvalue, so we can assign to it
194  symbol.is_lvalue=true;
195 
196  failure_value=symbol.symbol_expr();
197  failure_value.set(ID_C_invalid_object, true);
198  }
199 
200  valuet value;
201  value.value=failure_value;
202  value.pointer_guard=true_exprt();
203  values.push_front(value);
204  }
205 
206  // now build big case split, but we only do "good" objects
207 
208  exprt value=nil_exprt();
209 
210  for(std::list<valuet>::const_iterator
211  it=values.begin();
212  it!=values.end();
213  it++)
214  {
215  if(it->value.is_not_nil())
216  {
217  if(value.is_nil()) // first?
218  value=it->value;
219  else
220  value=if_exprt(it->pointer_guard, it->value, value);
221  }
222  }
223 
224  if(compare_against_pointer != pointer)
225  value = let_exprt(to_symbol_expr(compare_against_pointer), pointer, value);
226 
227 #ifdef DEBUG
228  std::cout << "value_set_derefencet::dereference value=" << format(value)
229  << '\n'
230  << std::flush;
231 #endif
232 
233  return value;
234 }
235 
245  const typet &object_type,
246  const typet &dereference_type,
247  const namespacet &ns)
248 {
249  const typet *object_unwrapped = &object_type;
250  const typet *dereference_unwrapped = &dereference_type;
251  while(object_unwrapped->id() == ID_pointer &&
252  dereference_unwrapped->id() == ID_pointer)
253  {
254  object_unwrapped = &object_unwrapped->subtype();
255  dereference_unwrapped = &dereference_unwrapped->subtype();
256  }
257  if(dereference_unwrapped->id() == ID_empty)
258  {
259  return true;
260  }
261  else if(dereference_unwrapped->id() == ID_pointer &&
262  object_unwrapped->id() != ID_pointer)
263  {
264 #ifdef DEBUG
265  std::cout << "value_set_dereference: the dereference type has "
266  "too many ID_pointer levels"
267  << std::endl;
268  std::cout << " object_type: " << object_type.pretty() << std::endl;
269  std::cout << " dereference_type: " << dereference_type.pretty()
270  << std::endl;
271 #endif
272  }
273 
274  if(object_type == dereference_type)
275  return true; // ok, they just match
276 
277  // check for struct prefixes
278 
279  const typet ot_base=ns.follow(object_type),
280  dt_base=ns.follow(dereference_type);
281 
282  if(ot_base.id()==ID_struct &&
283  dt_base.id()==ID_struct)
284  {
285  if(to_struct_type(dt_base).is_prefix_of(
286  to_struct_type(ot_base)))
287  return true; // ok, dt is a prefix of ot
288  }
289 
290  // we are generous about code pointers
291  if(dereference_type.id()==ID_code &&
292  object_type.id()==ID_code)
293  return true;
294 
295  // bitvectors of same width are ok
296  if((dereference_type.id()==ID_signedbv ||
297  dereference_type.id()==ID_unsignedbv) &&
298  (object_type.id()==ID_signedbv ||
299  object_type.id()==ID_unsignedbv) &&
300  to_bitvector_type(dereference_type).get_width()==
301  to_bitvector_type(object_type).get_width())
302  return true;
303 
304  // really different
305 
306  return false;
307 }
308 
323  const exprt &what,
324  bool exclude_null_derefs,
325  const irep_idt &language_mode)
326 {
327  if(what.id() == ID_unknown || what.id() == ID_invalid)
328  {
329  return false;
330  }
331 
333 
334  const exprt &root_object = o.root_object();
335  if(root_object.id() == ID_null_object)
336  {
337  return exclude_null_derefs;
338  }
339  else if(root_object.id() == ID_integer_address)
340  {
341  return language_mode == ID_java;
342  }
343 
344  return false;
345 }
346 
360  const exprt &what,
361  const exprt &pointer_expr,
362  const namespacet &ns)
363 {
364  const pointer_typet &pointer_type =
365  type_checked_cast<pointer_typet>(pointer_expr.type());
366  const typet &dereference_type = pointer_type.subtype();
367 
368  if(what.id()==ID_unknown ||
369  what.id()==ID_invalid)
370  {
371  return valuet();
372  }
373 
374  if(what.id()!=ID_object_descriptor)
375  throw "unknown points-to: "+what.id_string();
376 
378 
379  const exprt &root_object=o.root_object();
380  const exprt &object=o.object();
381 
382  #if 0
383  std::cout << "O: " << format(root_object) << '\n';
384  #endif
385 
386  valuet result;
387 
388  if(root_object.id() == ID_null_object)
389  {
390  if(o.offset().is_zero())
392  else
393  return valuet{};
394  }
395  else if(root_object.id()==ID_dynamic_object)
396  {
397  // constraint that it actually is a dynamic object
398  // this is also our guard
399  result.pointer_guard = dynamic_object(pointer_expr);
400 
401  // can't remove here, turn into *p
402  result.value = dereference_exprt{pointer_expr};
403  result.pointer = pointer_expr;
404  }
405  else if(root_object.id()==ID_integer_address)
406  {
407  // This is stuff like *((char *)5).
408  // This is turned into an access to __CPROVER_memory[...].
409 
410  const symbolt &memory_symbol=ns.lookup(CPROVER_PREFIX "memory");
411  const symbol_exprt symbol_expr(memory_symbol.name, memory_symbol.type);
412 
413  if(memory_symbol.type.subtype() == dereference_type)
414  {
415  // Types match already, what a coincidence!
416  // We can use an index expression.
417 
418  const index_exprt index_expr(
419  symbol_expr,
420  pointer_offset(pointer_expr),
421  memory_symbol.type.subtype());
422 
423  result.value=index_expr;
424  result.pointer = address_of_exprt{index_expr};
425  }
426  else if(
428  memory_symbol.type.subtype(), dereference_type, ns))
429  {
430  const index_exprt index_expr(
431  symbol_expr,
432  pointer_offset(pointer_expr),
433  memory_symbol.type.subtype());
434  result.value=typecast_exprt(index_expr, dereference_type);
435  result.pointer =
437  }
438  else
439  {
440  // We need to use byte_extract.
441  // Won't do this without a commitment to an endianness.
442 
444  {
445  }
446  else
447  {
448  result.value = byte_extract_exprt(
449  byte_extract_id(),
450  symbol_expr,
451  pointer_offset(pointer_expr),
452  dereference_type);
453  result.pointer = address_of_exprt{result.value};
454  }
455  }
456  }
457  else
458  {
459  // something generic -- really has to be a symbol
460  address_of_exprt object_pointer(object);
461 
462  if(o.offset().is_zero())
463  {
464  result.pointer_guard = equal_exprt(
465  typecast_exprt::conditional_cast(pointer_expr, object_pointer.type()),
466  object_pointer);
467  }
468  else
469  {
470  result.pointer_guard=same_object(pointer_expr, object_pointer);
471  }
472 
473  const typet &object_type = object.type();
474  const typet &root_object_type = root_object.type();
475 
476  exprt root_object_subexpression=root_object;
477 
478  if(
479  dereference_type_compare(object_type, dereference_type, ns) &&
480  o.offset().is_zero())
481  {
482  // The simplest case: types match, and offset is zero!
483  // This is great, we are almost done.
484 
485  result.value = typecast_exprt::conditional_cast(object, dereference_type);
486  result.pointer =
488  }
489  else if(
490  root_object_type.id() == ID_array &&
492  root_object_type.subtype(), dereference_type, ns))
493  {
494  // We have an array with a subtype that matches
495  // the dereferencing type.
496  // We will require well-alignedness!
497 
498  exprt offset;
499 
500  // this should work as the object is essentially the root object
501  if(o.offset().is_constant())
502  offset=o.offset();
503  else
504  offset=pointer_offset(pointer_expr);
505 
506  exprt adjusted_offset;
507 
508  // are we doing a byte?
509  auto element_size = pointer_offset_size(root_object_type.subtype(), ns);
510 
511  if(!element_size.has_value() || *element_size == 0)
512  {
513  throw "unknown or invalid type size of:\n" +
514  root_object_type.subtype().pretty();
515  }
516  else if(*element_size == 1)
517  {
518  // no need to adjust offset
519  adjusted_offset = offset;
520  }
521  else
522  {
523  exprt element_size_expr = from_integer(*element_size, offset.type());
524 
525  adjusted_offset=binary_exprt(
526  offset, ID_div, element_size_expr, offset.type());
527 
528  // TODO: need to assert well-alignedness
529  }
530 
531  const index_exprt &index_expr =
532  index_exprt(root_object, adjusted_offset, root_object_type.subtype());
533  result.value =
534  typecast_exprt::conditional_cast(index_expr, dereference_type);
536  address_of_exprt{index_expr}, pointer_type);
537  }
538  else
539  {
540  // try to build a member/index expression - do not use byte_extract
541  auto subexpr = get_subexpression_at_offset(
542  root_object_subexpression, o.offset(), dereference_type, ns);
543  if(subexpr.has_value())
544  simplify(subexpr.value(), ns);
545  if(subexpr.has_value() && subexpr.value().id() != byte_extract_id())
546  {
547  // Successfully found a member, array index, or combination thereof
548  // that matches the desired type and offset:
549  result.value = subexpr.value();
551  address_of_exprt{skip_typecast(subexpr.value())}, pointer_type);
552  return result;
553  }
554 
555  // we extract something from the root object
556  result.value=o.root_object();
559 
560  // this is relative to the root object
561  exprt offset;
562  if(o.offset().id()==ID_unknown)
563  offset=pointer_offset(pointer_expr);
564  else
565  offset=o.offset();
566 
567  if(memory_model(result.value, dereference_type, offset, ns))
568  {
569  // ok, done
570  }
571  else
572  {
573  return valuet(); // give up, no way that this is ok
574  }
575  }
576  }
577 
578  return result;
579 }
580 
581 static bool is_a_bv_type(const typet &type)
582 {
583  return type.id()==ID_unsignedbv ||
584  type.id()==ID_signedbv ||
585  type.id()==ID_bv ||
586  type.id()==ID_fixedbv ||
587  type.id()==ID_floatbv ||
588  type.id()==ID_c_enum_tag;
589 }
590 
600  exprt &value,
601  const typet &to_type,
602  const exprt &offset,
603  const namespacet &ns)
604 {
605  // we will allow more or less arbitrary pointer type cast
606 
607  const typet from_type=value.type();
608 
609  // first, check if it's really just a type coercion,
610  // i.e., both have exactly the same (constant) size,
611  // for bit-vector types or pointers
612 
613  if(
614  (is_a_bv_type(from_type) && is_a_bv_type(to_type)) ||
615  (from_type.id() == ID_pointer && to_type.id() == ID_pointer))
616  {
618  {
619  // avoid semantic conversion in case of
620  // cast to float or fixed-point,
621  // or cast from float or fixed-point
622 
623  if(
624  to_type.id() != ID_fixedbv && to_type.id() != ID_floatbv &&
625  from_type.id() != ID_fixedbv && from_type.id() != ID_floatbv)
626  {
627  value = typecast_exprt::conditional_cast(value, to_type);
628  return true;
629  }
630  }
631  }
632 
633  // otherwise, we will stitch it together from bytes
634 
635  return memory_model_bytes(value, to_type, offset, ns);
636 }
637 
647  exprt &value,
648  const typet &to_type,
649  const exprt &offset,
650  const namespacet &ns)
651 {
652  const typet from_type=value.type();
653 
654  // We simply refuse to convert to/from code.
655  if(from_type.id()==ID_code || to_type.id()==ID_code)
656  return false;
657 
658  // We won't do this without a commitment to an endianness.
660  return false;
661 
662  // But everything else we will try!
663  // We just rely on byte_extract to do the job!
664 
665  exprt result;
666 
667  // See if we have an array of bytes already,
668  // and we want something byte-sized.
669  auto from_type_subtype_size = pointer_offset_size(from_type.subtype(), ns);
670 
671  auto to_type_size = pointer_offset_size(to_type, ns);
672 
673  if(
674  from_type.id() == ID_array && from_type_subtype_size.has_value() &&
675  *from_type_subtype_size == 1 && to_type_size.has_value() &&
676  *to_type_size == 1 && is_a_bv_type(from_type.subtype()) &&
677  is_a_bv_type(to_type))
678  {
679  // yes, can use 'index', but possibly need to convert
681  index_exprt(value, offset, from_type.subtype()), to_type);
682  }
683  else
684  {
685  // no, use 'byte_extract'
686  result = byte_extract_exprt(byte_extract_id(), value, offset, to_type);
687  }
688 
689  value=result;
690 
691  return true;
692 }
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.
format
static format_containert< T > format(const T &o)
Definition: format.h:35
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
value_set_dereferencet::valuet
Return value for build_reference_to; see that method for documentation.
Definition: value_set_dereference.h:59
skip_typecast
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
Definition: expr_util.cpp:217
dereference_callbackt::get_value_set
virtual void get_value_set(const exprt &expr, value_setst::valuest &value_set) const =0
arith_tools.h
value_set_dereferencet::valuet::pointer_guard
exprt pointer_guard
Definition: value_set_dereference.h:63
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:303
value_set_dereferencet::memory_model
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...
Definition: value_set_dereference.cpp:599
exprt::depth_begin
depth_iteratort depth_begin()
Definition: expr.cpp:331
value_set_dereferencet::ns
const namespacet & ns
Definition: value_set_dereference.h:99
typet
The type of an expression, extends irept.
Definition: type.h:29
fresh_symbol.h
Fresh auxiliary symbol creation.
irept::pretty
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:488
to_if_expr
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:3029
value_set_dereference.h
Pointer Dereferencing.
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
dereference_exprt
Operator to dereference a pointer.
Definition: std_expr.h:2888
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:2964
pointer_predicates.h
Various predicates over pointers in programs.
value_set_dereferencet::language_mode
const irep_idt language_mode
language_mode: ID_java, ID_C or another language identifier if we know the source language in use,...
Definition: value_set_dereference.h:104
object_descriptor_exprt
Split an expression into a base object and a (byte) offset.
Definition: std_expr.h:1832
value_set_dereferencet::should_ignore_value
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.
Definition: value_set_dereference.cpp:322
value_set_dereferencet::exclude_null_derefs
const bool exclude_null_derefs
Flag indicating whether value_set_dereferencet::dereference should disregard an apparent attempt to d...
Definition: value_set_dereference.h:107
exprt
Base class for all expressions.
Definition: expr.h:53
binary_exprt
A base class for binary expressions.
Definition: std_expr.h:601
from_type
std::string from_type(const namespacet &ns, const irep_idt &identifier, const typet &type)
Definition: language_util.cpp:33
options.h
Options.
dereference_callbackt::get_or_create_failed_symbol
virtual const symbolt * get_or_create_failed_symbol(const exprt &expr)=0
dynamic_object
exprt dynamic_object(const exprt &pointer)
Definition: pointer_predicates.cpp:71
value_set_dereferencet::dereference_type_compare
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...
Definition: value_set_dereference.cpp:244
configt::ansi_c
struct configt::ansi_ct ansi_c
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
equal_exprt
Equality.
Definition: std_expr.h:1190
if_exprt::false_case
exprt & false_case()
Definition: std_expr.h:3001
value_set_dereferencet::new_symbol_table
symbol_tablet & new_symbol_table
Definition: value_set_dereference.h:100
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
configt::ansi_ct::endiannesst::NO_ENDIANNESS
@ NO_ENDIANNESS
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
value_set_dereferencet::dereference
exprt dereference(const exprt &pointer)
Dereference the given pointer-expression.
Definition: value_set_dereference.cpp:63
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:140
byte_operators.h
Expression classes for byte-level operators.
null_pointer_exprt
The null pointer constant.
Definition: std_expr.h:3989
value_set_dereferencet::valuet::pointer
exprt pointer
Definition: value_set_dereference.h:62
should_use_local_definition_for
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...
Definition: value_set_dereference.cpp:46
nil_exprt
The NIL expression.
Definition: std_expr.h:3973
pointer_offset_bits
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
Definition: pointer_offset_size.cpp:100
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:122
value_set_dereferencet::dereference_callback
dereference_callbackt & dereference_callback
Definition: value_set_dereference.h:101
to_object_descriptor_expr
const object_descriptor_exprt & to_object_descriptor_expr(const exprt &expr)
Cast an exprt to an object_descriptor_exprt.
Definition: std_expr.h:1898
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
pointer_type
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:177
irept::is_nil
bool is_nil() const
Definition: irep.h:398
irept::id
const irep_idt & id() const
Definition: irep.h:418
range.h
Ranges: pair of begin and end iterators, which can be initialized from containers,...
value_set_dereferencet::memory_model_bytes
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...
Definition: value_set_dereference.cpp:646
unary_exprt::op
const exprt & op() const
Definition: std_expr.h:281
cprover_prefix.h
object_descriptor_exprt::root_object
const exprt & root_object() const
Definition: std_expr.cpp:218
pointer_offset
exprt pointer_offset(const exprt &pointer)
Definition: pointer_predicates.cpp:37
config
configt config
Definition: config.cpp:24
source_locationt
Definition: source_location.h:20
simplify_expr.h
exprt::is_zero
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:132
expr_util.h
Deprecated expression utility functions.
ssa_expr.h
format_expr.h
is_a_bv_type
static bool is_a_bv_type(const typet &type)
Definition: value_set_dereference.cpp:581
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
expr_iterator.h
Forward depth-first search iterators These iterators' copy operations are expensive,...
if_exprt::true_case
exprt & true_case()
Definition: std_expr.h:2991
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:51
symbolt
Symbol table entry.
Definition: symbol.h:28
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
to_typecast_expr
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:2047
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
exprt::is_constant
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:85
if_exprt::cond
exprt & cond()
Definition: std_expr.h:2981
CPROVER_PREFIX
#define CPROVER_PREFIX
Definition: cprover_prefix.h:14
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
same_object
exprt same_object(const exprt &p1, const exprt &p2)
Definition: pointer_predicates.cpp:27
value_set_dereferencet::build_reference_to
static valuet build_reference_to(const exprt &what, const exprt &pointer, const namespacet &ns)
Definition: value_set_dereference.cpp:359
config.h
symbolt::is_lvalue
bool is_lvalue
Definition: symbol.h:66
index_exprt
Array index operator.
Definition: std_expr.h:1293
address_of_exprt
Operator to return the address of an object.
Definition: std_expr.h:2786
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:2013
pointer_typet
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: std_types.h:1488
object_descriptor_exprt::object
exprt & object()
Definition: std_expr.h:1858
true_exprt
The Boolean constant true.
Definition: std_expr.h:3955
exprt::depth_end
depth_iteratort depth_end()
Definition: expr.cpp:333
array_name.h
Misc Utilities.
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:254
make_range
ranget< iteratort > make_range(iteratort begin, iteratort end)
Definition: range.h:524
c_types.h
get_fresh_aux_symbol
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 ...
Definition: fresh_symbol.cpp:32
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
format_type.h
let_exprt
A let expression.
Definition: std_expr.h:4165
configt::ansi_ct::endianness
endiannesst endianness
Definition: config.h:77
to_bitvector_type
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
Definition: std_types.h:1089
value_set_dereferencet::valuet::value
exprt value
Definition: value_set_dereference.h:61
object_descriptor_exprt::offset
exprt & offset()
Definition: std_expr.h:1870