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/base_type.h>
22 #include <util/byte_operators.h>
23 #include <util/c_types.h>
24 #include <util/config.h>
25 #include <util/cprover_prefix.h>
26 #include <util/format_type.h>
27 #include <util/fresh_symbol.h>
28 #include <util/guard.h>
29 #include <util/options.h>
32 #include <util/ssa_expr.h>
33 
34 // global data, horrible
36 
38 {
39  if(expr.id()==ID_member || expr.id()==ID_index)
40  return get_symbol(expr.op0());
41 
42  return expr;
43 }
44 
49  const exprt &pointer,
50  const guardt &guard,
51  const modet mode)
52 {
53  if(pointer.type().id()!=ID_pointer)
54  throw "dereference expected pointer type, but got "+
55  pointer.type().pretty();
56 
57  // we may get ifs due to recursive calls
58  if(pointer.id()==ID_if)
59  {
60  const if_exprt &if_expr=to_if_expr(pointer);
61  // push down the if
62  guardt true_guard=guard;
63  guardt false_guard=guard;
64 
65  true_guard.add(if_expr.cond());
66  false_guard.add(not_exprt(if_expr.cond()));
67 
68  exprt true_case=dereference(if_expr.true_case(), true_guard, mode);
69  exprt false_case=dereference(if_expr.false_case(), false_guard, mode);
70 
71  return if_exprt(if_expr.cond(), true_case, false_case);
72  }
73 
74  // type of the object
75  const typet &type=pointer.type().subtype();
76 
77  #if 0
78  std::cout << "DEREF: " << format(pointer) << '\n';
79  #endif
80 
81  // collect objects the pointer may point to
82  value_setst::valuest points_to_set;
83 
84  dereference_callback.get_value_set(pointer, points_to_set);
85 
86  #if 0
87  for(value_setst::valuest::const_iterator
88  it=points_to_set.begin();
89  it!=points_to_set.end();
90  it++)
91  std::cout << "P: " << format(*it) << '\n';
92  #endif
93 
94  // get the values of these
95 
96  std::list<valuet> values;
97 
98  for(value_setst::valuest::const_iterator
99  it=points_to_set.begin();
100  it!=points_to_set.end();
101  it++)
102  {
103  valuet value=build_reference_to(*it, mode, pointer, guard);
104 
105  #if 0
106  std::cout << "V: " << format(value.pointer_guard) << " --> ";
107  std::cout << format(value.value);
108  if(value.ignore)
109  std::cout << " (ignored)";
110  std::cout << '\n';
111  #endif
112 
113  if(!value.ignore)
114  values.push_back(value);
115  }
116 
117  // can this fail?
118  bool may_fail;
119 
120  if(values.empty())
121  {
122  invalid_pointer(pointer, guard);
123  may_fail=true;
124  }
125  else
126  {
127  may_fail=false;
128  for(std::list<valuet>::const_iterator
129  it=values.begin();
130  it!=values.end();
131  it++)
132  if(it->value.is_nil())
133  may_fail=true;
134  }
135 
136  if(may_fail)
137  {
138  // first see if we have a "failed object" for this pointer
139 
140  const symbolt *failed_symbol;
141  exprt failure_value;
142 
144  pointer, failed_symbol))
145  {
146  // yes!
147  failure_value=failed_symbol->symbol_expr();
148  failure_value.set(ID_C_invalid_object, true);
149  }
150  else
151  {
152  // else: produce new symbol
153  symbolt &symbol = get_fresh_aux_symbol(
154  type,
155  "symex",
156  "invalid_object",
157  pointer.source_location(),
160 
161  // make it a lvalue, so we can assign to it
162  symbol.is_lvalue=true;
163 
164  failure_value=symbol.symbol_expr();
165  failure_value.set(ID_C_invalid_object, true);
166  }
167 
168  valuet value;
169  value.value=failure_value;
170  value.pointer_guard=true_exprt();
171  values.push_front(value);
172  }
173 
174  // now build big case split, but we only do "good" objects
175 
176  exprt value=nil_exprt();
177 
178  for(std::list<valuet>::const_iterator
179  it=values.begin();
180  it!=values.end();
181  it++)
182  {
183  if(it->value.is_not_nil())
184  {
185  if(value.is_nil()) // first?
186  value=it->value;
187  else
188  value=if_exprt(it->pointer_guard, it->value, value);
189  }
190  }
191 
192  #if 0
193  std::cout << "R: " << format(value) << "\n\n";
194  #endif
195 
196  return value;
197 }
198 
200  const typet &object_type,
201  const typet &dereference_type) const
202 {
203  // check if the two types have matching number of ID_pointer levels, with
204  // the dereference type eventually pointing to void; then this is ok
205  // for example:
206  // - dereference_type=void is ok (no matter what object_type is);
207  // - object_type=(int *), dereference_type=(void *) is ok;
208  // - object_type=(int **), dereference_type=(void **) is ok;
209  // - object_type=(int **), dereference_type=(void *) is ok;
210  // - object_type=(int *), dereference_type=(void **) is not ok;
211  const typet *object_unwrapped = &object_type;
212  const typet *dereference_unwrapped = &dereference_type;
213  while(object_unwrapped->id() == ID_pointer &&
214  dereference_unwrapped->id() == ID_pointer)
215  {
216  object_unwrapped = &object_unwrapped->subtype();
217  dereference_unwrapped = &dereference_unwrapped->subtype();
218  }
219  if(dereference_unwrapped->id() == ID_empty)
220  {
221  return true;
222  }
223  else if(dereference_unwrapped->id() == ID_pointer &&
224  object_unwrapped->id() != ID_pointer)
225  {
226 #ifdef DEBUG
227  std::cout << "value_set_dereference: the dereference type has "
228  "too many ID_pointer levels"
229  << std::endl;
230  std::cout << " object_type: " << object_type.pretty() << std::endl;
231  std::cout << " dereference_type: " << dereference_type.pretty()
232  << std::endl;
233 #endif
234  }
235 
236  if(base_type_eq(object_type, dereference_type, ns))
237  return true; // ok, they just match
238 
239  // check for struct prefixes
240 
241  const typet ot_base=ns.follow(object_type),
242  dt_base=ns.follow(dereference_type);
243 
244  if(ot_base.id()==ID_struct &&
245  dt_base.id()==ID_struct)
246  {
247  if(to_struct_type(dt_base).is_prefix_of(
248  to_struct_type(ot_base)))
249  return true; // ok, dt is a prefix of ot
250  }
251 
252  // we are generous about code pointers
253  if(dereference_type.id()==ID_code &&
254  object_type.id()==ID_code)
255  return true;
256 
257  // bitvectors of same width are ok
258  if((dereference_type.id()==ID_signedbv ||
259  dereference_type.id()==ID_unsignedbv) &&
260  (object_type.id()==ID_signedbv ||
261  object_type.id()==ID_unsignedbv) &&
262  to_bitvector_type(dereference_type).get_width()==
263  to_bitvector_type(object_type).get_width())
264  return true;
265 
266  // really different
267 
268  return false;
269 }
270 
272  const exprt &pointer,
273  const guardt &guard)
274 {
275  if(!options.get_bool_option("pointer-check"))
276  return;
277 
278  // constraint that it actually is an invalid pointer
279  guardt tmp_guard(guard);
280  tmp_guard.add(::invalid_pointer(pointer));
281 
283  "pointer dereference",
284  "invalid pointer",
285  tmp_guard);
286 }
287 
289  const exprt &what,
290  const modet mode,
291  const exprt &pointer_expr,
292  const guardt &guard)
293 {
294  const typet &dereference_type=
295  ns.follow(pointer_expr.type()).subtype();
296 
297  if(what.id()==ID_unknown ||
298  what.id()==ID_invalid)
299  {
300  invalid_pointer(pointer_expr, guard);
301  return valuet();
302  }
303 
304  if(what.id()!=ID_object_descriptor)
305  throw "unknown points-to: "+what.id_string();
306 
308 
309  const exprt &root_object=o.root_object();
310  const exprt &object=o.object();
311 
312  #if 0
313  std::cout << "O: " << format(root_object) << '\n';
314  #endif
315 
316  valuet result;
317 
318  if(root_object.id() == ID_null_object)
319  {
321  {
322  result.ignore = true;
323  }
324  else if(options.get_bool_option("pointer-check"))
325  {
326  guardt tmp_guard(guard);
327 
328  if(o.offset().is_zero())
329  {
330  tmp_guard.add(null_pointer(pointer_expr));
331 
333  "pointer dereference",
334  "NULL pointer", tmp_guard);
335  }
336  else
337  {
338  tmp_guard.add(null_object(pointer_expr));
339 
341  "pointer dereference",
342  "NULL plus offset pointer", tmp_guard);
343  }
344  }
345  }
346  else if(root_object.id()==ID_dynamic_object)
347  {
348  // const dynamic_object_exprt &dynamic_object=
349  // to_dynamic_object_expr(root_object);
350 
351  // the object produced by malloc
353  ns.lookup(CPROVER_PREFIX "malloc_object").symbol_expr();
354 
355  exprt is_malloc_object=same_object(pointer_expr, malloc_object);
356 
357  // constraint that it actually is a dynamic object
358  // this is also our guard
359  result.pointer_guard = dynamic_object(pointer_expr);
360 
361  // can't remove here, turn into *p
362  result.value=dereference_exprt(pointer_expr, dereference_type);
363 
364  if(options.get_bool_option("pointer-check"))
365  {
366  // if(!dynamic_object.valid().is_true())
367  {
368  // check if it is still alive
369  guardt tmp_guard(guard);
370  tmp_guard.add(deallocated(pointer_expr, ns));
372  "pointer dereference",
373  "dynamic object deallocated",
374  tmp_guard);
375  }
376 
377  if(options.get_bool_option("bounds-check"))
378  {
379  if(!o.offset().is_zero())
380  {
381  // check lower bound
382  guardt tmp_guard(guard);
383  tmp_guard.add(is_malloc_object);
384  tmp_guard.add(
386  pointer_expr,
387  ns,
388  nil_exprt()));
390  "pointer dereference",
391  "dynamic object lower bound", tmp_guard);
392  }
393 
394  {
395  // check upper bound
396 
397  // we check SAME_OBJECT(__CPROVER_malloc_object, p) &&
398  // POINTER_OFFSET(p)+size>__CPROVER_malloc_size
399 
400  guardt tmp_guard(guard);
401  tmp_guard.add(is_malloc_object);
402  tmp_guard.add(
404  pointer_expr,
405  ns,
406  size_of_expr(dereference_type, ns)));
408  "pointer dereference",
409  "dynamic object upper bound", tmp_guard);
410  }
411  }
412  }
413  }
414  else if(root_object.id()==ID_integer_address)
415  {
416  // This is stuff like *((char *)5).
417  // This is turned into an access to __CPROVER_memory[...].
418 
419  if(language_mode == ID_java)
420  {
421  result.ignore = true;
422  return result;
423  }
424 
425  const symbolt &memory_symbol=ns.lookup(CPROVER_PREFIX "memory");
426  const symbol_exprt symbol_expr(memory_symbol.name, memory_symbol.type);
427 
428  if(base_type_eq(
429  ns.follow(memory_symbol.type).subtype(),
430  dereference_type, ns))
431  {
432  // Types match already, what a coincidence!
433  // We can use an index expression.
434 
435  const index_exprt index_expr(
436  symbol_expr,
437  pointer_offset(pointer_expr),
438  ns.follow(memory_symbol.type).subtype());
439  result.value=index_expr;
440  }
441  else if(dereference_type_compare(
442  ns.follow(memory_symbol.type).subtype(),
443  dereference_type))
444  {
445  const index_exprt index_expr(
446  symbol_expr,
447  pointer_offset(pointer_expr),
448  ns.follow(memory_symbol.type).subtype());
449  result.value=typecast_exprt(index_expr, dereference_type);
450  }
451  else
452  {
453  // We need to use byte_extract.
454  // Won't do this without a commitment to an endianness.
455 
457  {
458  }
459  else
460  {
461  result.value = byte_extract_exprt(
462  byte_extract_id(),
463  symbol_expr,
464  pointer_offset(pointer_expr),
465  dereference_type);
466  }
467  }
468  }
469  else
470  {
471  // something generic -- really has to be a symbol
472  address_of_exprt object_pointer(object);
473 
474  if(o.offset().is_zero())
475  {
476  equal_exprt equality(pointer_expr, object_pointer);
477 
478  if(ns.follow(equality.lhs().type())!=ns.follow(equality.rhs().type()))
479  equality.lhs().make_typecast(equality.rhs().type());
480 
481  result.pointer_guard=equality;
482  }
483  else
484  {
485  result.pointer_guard=same_object(pointer_expr, object_pointer);
486  }
487 
488  guardt tmp_guard(guard);
489  tmp_guard.add(result.pointer_guard);
490 
491  valid_check(object, tmp_guard, mode);
492 
493  const typet &object_type=ns.follow(object.type());
494  const exprt &root_object=o.root_object();
495  const typet &root_object_type=ns.follow(root_object.type());
496 
497  exprt root_object_subexpression=root_object;
498 
499  if(dereference_type_compare(object_type, dereference_type) &&
500  o.offset().is_zero())
501  {
502  // The simplest case: types match, and offset is zero!
503  // This is great, we are almost done.
504 
505  result.value=object;
506 
507  if(object_type!=ns.follow(dereference_type))
508  result.value.make_typecast(dereference_type);
509  }
510  else if(root_object_type.id()==ID_array &&
512  root_object_type.subtype(),
513  dereference_type))
514  {
515  // We have an array with a subtype that matches
516  // the dereferencing type.
517  // We will require well-alignedness!
518 
519  exprt offset;
520 
521  // this should work as the object is essentially the root object
522  if(o.offset().is_constant())
523  offset=o.offset();
524  else
525  offset=pointer_offset(pointer_expr);
526 
527  exprt adjusted_offset;
528 
529  // are we doing a byte?
530  mp_integer element_size =
531  pointer_offset_size(root_object_type.subtype(), ns);
532 
533  if(element_size==1)
534  {
535  // no need to adjust offset
536  adjusted_offset=offset;
537  }
538  else if(element_size<=0)
539  {
540  throw "unknown or invalid type size of:\n" +
541  root_object_type.subtype().pretty();
542  }
543  else
544  {
545  exprt element_size_expr=
546  from_integer(element_size, offset.type());
547 
548  adjusted_offset=binary_exprt(
549  offset, ID_div, element_size_expr, offset.type());
550 
551  // TODO: need to assert well-alignedness
552  }
553 
554  index_exprt index_expr=
555  index_exprt(root_object, adjusted_offset, root_object_type.subtype());
556 
557  bounds_check(index_expr, tmp_guard);
558 
559  result.value=index_expr;
560 
561  if(ns.follow(result.value.type())!=ns.follow(dereference_type))
562  result.value.make_typecast(dereference_type);
563  }
565  root_object_subexpression,
566  o.offset(),
567  dereference_type,
568  ns))
569  {
570  // Successfully found a member, array index, or combination thereof
571  // that matches the desired type and offset:
572  result.value=root_object_subexpression;
573  }
574  else
575  {
576  // we extract something from the root object
577  result.value=o.root_object();
578 
579  // this is relative to the root object
580  exprt offset;
581  if(o.offset().id()==ID_unknown)
582  offset=pointer_offset(pointer_expr);
583  else
584  offset=o.offset();
585 
586  if(memory_model(result.value, dereference_type, tmp_guard, offset))
587  {
588  // ok, done
589  }
590  else
591  {
592  if(options.get_bool_option("pointer-check"))
593  {
594  std::ostringstream msg;
595  msg << "memory model not applicable (got `"
596  << format(result.value.type()) << "', expected `"
597  << format(dereference_type) << "')";
598 
600  "pointer dereference", msg.str(), tmp_guard);
601  }
602 
603  return valuet(); // give up, no way that this is ok
604  }
605  }
606  }
607 
608  return result;
609 }
610 
612  const exprt &object,
613  const guardt &guard,
614  const modet mode)
615 {
616  if(!options.get_bool_option("pointer-check"))
617  return;
618 
619  const exprt &symbol_expr=get_symbol(object);
620 
621  if(symbol_expr.id()==ID_string_constant)
622  {
623  // always valid, but can't write
624 
625  if(mode==modet::WRITE)
626  {
628  "pointer dereference",
629  "write access to string constant",
630  guard);
631  }
632  }
633  else if(symbol_expr.is_nil() ||
634  symbol_expr.get_bool(ID_C_invalid_object))
635  {
636  // always "valid", shut up
637  return;
638  }
639  else if(symbol_expr.id()==ID_symbol)
640  {
641  const irep_idt identifier=
642  is_ssa_expr(symbol_expr)?
643  to_ssa_expr(symbol_expr).get_object_name():
644  to_symbol_expr(symbol_expr).get_identifier();
645 
646  const symbolt &symbol=ns.lookup(identifier);
647 
648  if(symbol.type.get_bool(ID_C_is_failed_symbol))
649  {
651  "pointer dereference",
652  "invalid pointer",
653  guard);
654  }
655 
656  #if 0
657  if(dereference_callback.is_valid_object(identifier))
658  return; // always ok
659  #endif
660  }
661 }
662 
664  const index_exprt &expr,
665  const guardt &guard)
666 {
667  if(!options.get_bool_option("pointer-check"))
668  return;
669 
670  if(!options.get_bool_option("bounds-check"))
671  return;
672 
673  const typet &array_type=ns.follow(expr.op0().type());
674 
675  if(array_type.id()!=ID_array)
676  throw "bounds check expected array type";
677 
678  std::string name=array_name(ns, expr.array());
679 
680  {
681  mp_integer i;
682  if(!to_integer(expr.index(), i) &&
683  i>=0)
684  {
685  }
686  else
687  {
688  exprt zero=from_integer(0, expr.index().type());
689 
690  if(zero.is_nil())
691  throw "no zero constant of index type "+
692  expr.index().type().pretty();
693 
695  inequality(expr.index(), ID_lt, zero);
696 
697  guardt tmp_guard(guard);
698  tmp_guard.add(inequality);
700  "array bounds",
701  name+" lower bound", tmp_guard);
702  }
703  }
704 
705  const exprt &size_expr=
706  to_array_type(array_type).size();
707 
708  if(size_expr.id()==ID_infinity)
709  {
710  }
711  else if(size_expr.is_zero() && expr.array().id()==ID_member)
712  {
713  // this is a variable-sized struct field
714  }
715  else
716  {
717  if(size_expr.is_nil())
718  throw "index array operand of wrong type";
719 
720  binary_relation_exprt inequality(
721  typecast_exprt::conditional_cast(expr.index(), size_expr.type()),
722  ID_ge,
723  size_expr);
724 
725  guardt tmp_guard(guard);
726  tmp_guard.add(inequality);
728  "array bounds",
729  name+" upper bound", tmp_guard);
730  }
731 }
732 
733 static bool is_a_bv_type(const typet &type)
734 {
735  return type.id()==ID_unsignedbv ||
736  type.id()==ID_signedbv ||
737  type.id()==ID_bv ||
738  type.id()==ID_fixedbv ||
739  type.id()==ID_floatbv ||
740  type.id()==ID_c_enum_tag;
741 }
742 
744  exprt &value,
745  const typet &to_type,
746  const guardt &guard,
747  const exprt &offset)
748 {
749  // we will allow more or less arbitrary pointer type cast
750 
751  const typet from_type=value.type();
752 
753  // first, check if it's really just a type coercion,
754  // i.e., both have exactly the same (constant) size
755 
756  if(is_a_bv_type(from_type) &&
757  is_a_bv_type(to_type))
758  {
760  {
761  // avoid semantic conversion in case of
762  // cast to float or fixed-point,
763  // or cast from float or fixed-point
764 
765  if(to_type.id()==ID_fixedbv || to_type.id()==ID_floatbv ||
766  from_type.id()==ID_fixedbv || from_type.id()==ID_floatbv)
767  {
768  }
769  else
770  return memory_model_conversion(value, to_type, guard, offset);
771  }
772  }
773 
774  // we are willing to do the same for pointers
775 
776  if(from_type.id()==ID_pointer &&
777  to_type.id()==ID_pointer)
778  {
780  return memory_model_conversion(value, to_type, guard, offset);
781  }
782 
783  // otherwise, we will stitch it together from bytes
784 
785  return memory_model_bytes(value, to_type, guard, offset);
786 }
787 
789  exprt &value,
790  const typet &to_type,
791  const guardt &guard,
792  const exprt &offset)
793 {
794  // only doing type conversion
795  // just do the typecast
796  value.make_typecast(to_type);
797 
798  // also assert that offset is zero
799 
800  if(options.get_bool_option("pointer-check"))
801  {
802  equal_exprt offset_not_zero(offset, from_integer(0, offset.type()));
803  offset_not_zero.make_not();
804 
805  guardt tmp_guard(guard);
806  tmp_guard.add(offset_not_zero);
808  "word bounds",
809  "offset not zero", tmp_guard);
810  }
811 
812  return true;
813 }
814 
816  exprt &value,
817  const typet &to_type,
818  const guardt &guard,
819  const exprt &offset)
820 {
821  const typet from_type=value.type();
822 
823  // We simply refuse to convert to/from code.
824  if(from_type.id()==ID_code || to_type.id()==ID_code)
825  return false;
826 
827  // We won't do this without a commitment to an endianness.
829  return false;
830 
831  // But everything else we will try!
832  // We just rely on byte_extract to do the job!
833 
834  exprt result;
835 
836  // See if we have an array of bytes already,
837  // and we want something byte-sized.
838  if(ns.follow(from_type).id()==ID_array &&
840  pointer_offset_size(to_type, ns)==1 &&
842  is_a_bv_type(to_type))
843  {
844  // yes, can use 'index'
845  result=index_exprt(value, offset, ns.follow(from_type).subtype());
846 
847  // possibly need to convert
848  if(!base_type_eq(result.type(), to_type, ns))
849  result.make_typecast(to_type);
850  }
851  else
852  {
853  // no, use 'byte_extract'
854  result = byte_extract_exprt(byte_extract_id(), value, offset, to_type);
855  }
856 
857  value=result;
858 
859  // are we within the bounds?
860  if(options.get_bool_option("pointer-check"))
861  {
862  // upper bound
863  {
864  exprt from_width=size_of_expr(from_type, ns);
865  INVARIANT(
866  from_width.is_not_nil(),
867  "unknown or invalid type size:\n"+from_type.pretty());
868 
869  exprt to_width=
870  to_type.id()==ID_empty?
871  from_integer(0, size_type()):size_of_expr(to_type, ns);
872  INVARIANT(
873  to_width.is_not_nil(),
874  "unknown or invalid type size:\n"+to_type.pretty());
875  INVARIANT(
876  from_width.type()==to_width.type(),
877  "type mismatch on result of size_of_expr");
878 
879  minus_exprt bound(from_width, to_width);
880  if(bound.type()!=offset.type())
881  bound.make_typecast(offset.type());
882 
884  offset_upper_bound(offset, ID_gt, bound);
885 
886  guardt tmp_guard(guard);
887  tmp_guard.add(offset_upper_bound);
889  "pointer dereference",
890  "object upper bound", tmp_guard);
891  }
892 
893  // lower bound is easy
894  if(!offset.is_zero())
895  {
897  offset_lower_bound(
898  offset, ID_lt, from_integer(0, offset.type()));
899 
900  guardt tmp_guard(guard);
901  tmp_guard.add(offset_lower_bound);
903  "pointer dereference",
904  "object lower bound", tmp_guard);
905  }
906  }
907 
908  return true;
909 }
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
Definition: std_expr.h:3424
The type of an expression.
Definition: type.h:22
irep_idt name
The unique identifier.
Definition: symbol.h:43
exprt size_of_expr(const typet &type, const namespacet &ns)
struct configt::ansi_ct ansi_c
Boolean negation.
Definition: std_expr.h:3228
exprt & true_case()
Definition: std_expr.h:3393
semantic type conversion
Definition: std_expr.h:2111
BigInt mp_integer
Definition: mp_arith.h:22
bool is_nil() const
Definition: irep.h:172
A generic base class for relations, i.e., binary predicates.
Definition: std_expr.h:752
bool is_not_nil() const
Definition: irep.h:173
exprt & op0()
Definition: expr.h:72
static const exprt & get_symbol(const exprt &object)
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:641
#define CPROVER_PREFIX
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a generic typet to a bitvector_typet.
Definition: std_types.h:1159
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Definition: base_type.cpp:326
virtual exprt dereference(const exprt &pointer, const guardt &guard, const modet mode)
virtual void dereference_failure(const std::string &property, const std::string &msg, const guardt &guard)=0
dereference_callbackt & dereference_callback
const irep_idt & get_identifier() const
Definition: std_expr.h:128
endiannesst endianness
Definition: config.h:76
Fresh auxiliary symbol creation.
const object_descriptor_exprt & to_object_descriptor_expr(const exprt &expr)
Cast a generic exprt to an object_descriptor_exprt.
Definition: std_expr.h:2000
void invalid_pointer(const exprt &expr, const guardt &guard)
const exprt & root_object() const
Definition: std_expr.h:1966
The trinary if-then-else operator.
Definition: std_expr.h:3359
exprt & cond()
Definition: std_expr.h:3383
Definition: guard.h:19
mp_integer pointer_offset_bits(const typet &type, const namespacet &ns)
typet & type()
Definition: expr.h:56
unsignedbv_typet size_type()
Definition: c_types.cpp:58
bool memory_model(exprt &value, const typet &type, const guardt &guard, const exprt &offset)
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:240
Pointer Dereferencing.
configt config
Definition: config.cpp:23
virtual bool has_failed_symbol(const exprt &expr, const symbolt *&symbol)=0
exprt deallocated(const exprt &pointer, const namespacet &ns)
mp_integer pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
exprt null_object(const exprt &pointer)
void valid_check(const exprt &expr, const guardt &guard, const modet mode)
exprt dynamic_object_upper_bound(const exprt &pointer, const namespacet &ns, const exprt &access_size)
#define INVARIANT(CONDITION, REASON)
Definition: invariant.h:204
equality
Definition: std_expr.h:1354
const irep_idt & id() const
Definition: irep.h:259
void bounds_check(const index_exprt &expr, const guardt &guard)
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition: ssa_expr.h:154
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
Definition: symbol.cpp:111
Expression classes for byte-level operators.
The boolean constant true.
Definition: std_expr.h:4486
bool memory_model_bytes(exprt &value, const typet &type, const guardt &guard, const exprt &offset)
A generic base class for binary expressions.
Definition: std_expr.h:649
The NIL expression.
Definition: std_expr.h:4508
bool get_subexpression_at_offset(exprt &result, mp_integer offset, const typet &target_type_raw, const namespacet &ns)
Operator to dereference a pointer.
Definition: std_expr.h:3282
bool get_bool_option(const std::string &option) const
Definition: options.cpp:42
irep_idt byte_extract_id()
split an expression into a base object and a (byte) offset
Definition: std_expr.h:1945
const exprt & size() const
Definition: std_types.h:1023
Guard Data Structure.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:210
const typet & follow(const typet &) const
Definition: namespace.cpp:55
static bool is_a_bv_type(const typet &type)
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
Definition: std_types.h:318
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
valuet build_reference_to(const exprt &what, const modet mode, const exprt &pointer, const guardt &guard)
Get a guard and expression to access what under guard.
Operator to return the address of an object.
Definition: std_expr.h:3168
exprt & false_case()
Definition: std_expr.h:3403
Various predicates over pointers in programs.
exprt dynamic_object_lower_bound(const exprt &pointer, const namespacet &ns, const exprt &offset)
std::string from_type(const namespacet &ns, const irep_idt &identifier, const typet &type)
bool is_constant() const
Definition: expr.cpp:119
std::size_t get_width() const
Definition: std_types.h:1138
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:2124
Pointer Logic.
virtual void get_value_set(const exprt &expr, value_setst::valuest &value_set)=0
exprt malloc_object(const exprt &pointer, const namespacet &ns)
typet type
Type of symbol.
Definition: symbol.h:34
bool is_prefix_of(const struct_typet &other) const
Definition: std_types.cpp:76
void make_not()
Definition: expr.cpp:91
exprt & index()
Definition: std_expr.h:1496
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, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with the requested name pattern.
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Definition: std_types.h:1054
Base class for all expressions.
Definition: expr.h:42
exprt pointer_offset(const exprt &pointer)
irep_idt get_object_name() const
Definition: ssa_expr.h:46
const source_locationt & source_location() const
Definition: expr.h:125
bool is_ssa_expr(const exprt &expr)
Definition: ssa_expr.h:173
symbol_tablet & new_symbol_table
const std::string & id_string() const
Definition: irep.h:262
bool is_zero() const
Definition: expr.cpp:161
binary minus
Definition: std_expr.h:959
Expression to hold a symbol (variable)
Definition: std_expr.h:90
Options.
Misc Utilities.
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:17
exprt dynamic_object(const exprt &pointer)
exprt null_pointer(const exprt &pointer)
Base Type Computation.
const typet & subtype() const
Definition: type.h:33
TO_BE_DOCUMENTED.
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
const irep_idt language_mode
language_mode: ID_java, ID_C or another language identifier if we know the source language in use...
std::list< exprt > valuest
Definition: value_sets.h:28
exprt same_object(const exprt &p1, const exprt &p2)
bool memory_model_conversion(exprt &value, const typet &type, const guardt &guard, const exprt &offset)
exprt & array()
Definition: std_expr.h:1486
void make_typecast(const typet &_type)
Definition: expr.cpp:84
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
Definition: namespace.cpp:136
void add(const exprt &expr)
Definition: guard.cpp:64
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:286
const bool exclude_null_derefs
Flag indicating whether value_set_dereferencet::dereference should disregard an apparent attempt to d...
bool dereference_type_compare(const typet &object_type, const typet &dereference_type) const
std::string array_name(const namespacet &ns, const exprt &expr)
Definition: array_name.cpp:19
Return value for build_reference_to; see that method for documentation.
bool is_lvalue
Definition: symbol.h:68
array index operator
Definition: std_expr.h:1462
static format_containert< T > format(const T &o)
Definition: format.h:35