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) << '\n';
108  #endif
109 
110  values.push_back(value);
111  }
112 
113  // can this fail?
114  bool may_fail;
115 
116  if(values.empty())
117  {
118  invalid_pointer(pointer, guard);
119  may_fail=true;
120  }
121  else
122  {
123  may_fail=false;
124  for(std::list<valuet>::const_iterator
125  it=values.begin();
126  it!=values.end();
127  it++)
128  if(it->value.is_nil())
129  may_fail=true;
130  }
131 
132  if(may_fail)
133  {
134  // first see if we have a "failed object" for this pointer
135 
136  const symbolt *failed_symbol;
137  exprt failure_value;
138 
140  pointer, failed_symbol))
141  {
142  // yes!
143  failure_value=failed_symbol->symbol_expr();
144  failure_value.set(ID_C_invalid_object, true);
145  }
146  else
147  {
148  // else: produce new symbol
149  symbolt &symbol = get_fresh_aux_symbol(
150  type,
151  "symex",
152  "invalid_object",
153  pointer.source_location(),
156 
157  // make it a lvalue, so we can assign to it
158  symbol.is_lvalue=true;
159 
160  failure_value=symbol.symbol_expr();
161  failure_value.set(ID_C_invalid_object, true);
162  }
163 
164  valuet value;
165  value.value=failure_value;
166  value.pointer_guard=true_exprt();
167  values.push_front(value);
168  }
169 
170  // now build big case split, but we only do "good" objects
171 
172  exprt value=nil_exprt();
173 
174  for(std::list<valuet>::const_iterator
175  it=values.begin();
176  it!=values.end();
177  it++)
178  {
179  if(it->value.is_not_nil())
180  {
181  if(value.is_nil()) // first?
182  value=it->value;
183  else
184  value=if_exprt(it->pointer_guard, it->value, value);
185  }
186  }
187 
188  #if 0
189  std::cout << "R: " << format(value) << "\n\n";
190  #endif
191 
192  return value;
193 }
194 
196  const typet &object_type,
197  const typet &dereference_type) const
198 {
199  // check if the two types have matching number of ID_pointer levels, with
200  // the dereference type eventually pointing to void; then this is ok
201  // for example:
202  // - dereference_type=void is ok (no matter what object_type is);
203  // - object_type=(int *), dereference_type=(void *) is ok;
204  // - object_type=(int **), dereference_type=(void **) is ok;
205  // - object_type=(int **), dereference_type=(void *) is ok;
206  // - object_type=(int *), dereference_type=(void **) is not ok;
207  const typet *object_unwrapped = &object_type;
208  const typet *dereference_unwrapped = &dereference_type;
209  while(object_unwrapped->id() == ID_pointer &&
210  dereference_unwrapped->id() == ID_pointer)
211  {
212  object_unwrapped = &object_unwrapped->subtype();
213  dereference_unwrapped = &dereference_unwrapped->subtype();
214  }
215  if(dereference_unwrapped->id() == ID_empty)
216  {
217  return true;
218  }
219  else if(dereference_unwrapped->id() == ID_pointer &&
220  object_unwrapped->id() != ID_pointer)
221  {
222 #ifdef DEBUG
223  std::cout << "value_set_dereference: the dereference type has "
224  "too many ID_pointer levels"
225  << std::endl;
226  std::cout << " object_type: " << object_type.pretty() << std::endl;
227  std::cout << " dereference_type: " << dereference_type.pretty()
228  << std::endl;
229 #endif
230  }
231 
232  if(base_type_eq(object_type, dereference_type, ns))
233  return true; // ok, they just match
234 
235  // check for struct prefixes
236 
237  const typet ot_base=ns.follow(object_type),
238  dt_base=ns.follow(dereference_type);
239 
240  if(ot_base.id()==ID_struct &&
241  dt_base.id()==ID_struct)
242  {
243  if(to_struct_type(dt_base).is_prefix_of(
244  to_struct_type(ot_base)))
245  return true; // ok, dt is a prefix of ot
246  }
247 
248  // we are generous about code pointers
249  if(dereference_type.id()==ID_code &&
250  object_type.id()==ID_code)
251  return true;
252 
253  // bitvectors of same width are ok
254  if((dereference_type.id()==ID_signedbv ||
255  dereference_type.id()==ID_unsignedbv) &&
256  (object_type.id()==ID_signedbv ||
257  object_type.id()==ID_unsignedbv) &&
258  to_bitvector_type(dereference_type).get_width()==
259  to_bitvector_type(object_type).get_width())
260  return true;
261 
262  // really different
263 
264  return false;
265 }
266 
268  const exprt &pointer,
269  const guardt &guard)
270 {
271  if(!options.get_bool_option("pointer-check"))
272  return;
273 
274  // constraint that it actually is an invalid pointer
275  guardt tmp_guard(guard);
276  tmp_guard.add(::invalid_pointer(pointer));
277 
279  "pointer dereference",
280  "invalid pointer",
281  tmp_guard);
282 }
283 
285  const exprt &what,
286  const modet mode,
287  const exprt &pointer_expr,
288  const guardt &guard)
289 {
290  const typet &dereference_type=
291  ns.follow(pointer_expr.type()).subtype();
292 
293  if(what.id()==ID_unknown ||
294  what.id()==ID_invalid)
295  {
296  invalid_pointer(pointer_expr, guard);
297  return valuet();
298  }
299 
300  if(what.id()!=ID_object_descriptor)
301  throw "unknown points-to: "+what.id_string();
302 
304 
305  const exprt &root_object=o.root_object();
306  const exprt &object=o.object();
307 
308  #if 0
309  std::cout << "O: " << format(root_object) << '\n';
310  #endif
311 
312  valuet result;
313 
314  if(root_object.id() == ID_null_object)
315  {
316  if(options.get_bool_option("pointer-check"))
317  {
318  guardt tmp_guard(guard);
319 
320  if(o.offset().is_zero())
321  {
322  tmp_guard.add(null_pointer(pointer_expr));
323 
325  "pointer dereference",
326  "NULL pointer", tmp_guard);
327  }
328  else
329  {
330  tmp_guard.add(null_object(pointer_expr));
331 
333  "pointer dereference",
334  "NULL plus offset pointer", tmp_guard);
335  }
336  }
337  }
338  else if(root_object.id()==ID_dynamic_object)
339  {
340  // const dynamic_object_exprt &dynamic_object=
341  // to_dynamic_object_expr(root_object);
342 
343  // the object produced by malloc
345  ns.lookup(CPROVER_PREFIX "malloc_object").symbol_expr();
346 
347  exprt is_malloc_object=same_object(pointer_expr, malloc_object);
348 
349  // constraint that it actually is a dynamic object
350  // this is also our guard
351  result.pointer_guard = dynamic_object(pointer_expr);
352 
353  // can't remove here, turn into *p
354  result.value=dereference_exprt(pointer_expr, dereference_type);
355 
356  if(options.get_bool_option("pointer-check"))
357  {
358  // if(!dynamic_object.valid().is_true())
359  {
360  // check if it is still alive
361  guardt tmp_guard(guard);
362  tmp_guard.add(deallocated(pointer_expr, ns));
364  "pointer dereference",
365  "dynamic object deallocated",
366  tmp_guard);
367  }
368 
369  if(options.get_bool_option("bounds-check"))
370  {
371  if(!o.offset().is_zero())
372  {
373  // check lower bound
374  guardt tmp_guard(guard);
375  tmp_guard.add(is_malloc_object);
376  tmp_guard.add(
378  pointer_expr,
379  ns,
380  nil_exprt()));
382  "pointer dereference",
383  "dynamic object lower bound", tmp_guard);
384  }
385 
386  {
387  // check upper bound
388 
389  // we check SAME_OBJECT(__CPROVER_malloc_object, p) &&
390  // POINTER_OFFSET(p)+size>__CPROVER_malloc_size
391 
392  guardt tmp_guard(guard);
393  tmp_guard.add(is_malloc_object);
394  tmp_guard.add(
396  pointer_expr,
397  dereference_type,
398  ns,
399  size_of_expr(dereference_type, ns)));
401  "pointer dereference",
402  "dynamic object upper bound", tmp_guard);
403  }
404  }
405  }
406  }
407  else if(root_object.id()==ID_integer_address)
408  {
409  // This is stuff like *((char *)5).
410  // This is turned into an access to __CPROVER_memory[...].
411 
412  if(language_mode==ID_java)
413  {
414  result.value=nil_exprt();
415  return result;
416  }
417 
418  const symbolt &memory_symbol=ns.lookup(CPROVER_PREFIX "memory");
419  const symbol_exprt symbol_expr(memory_symbol.name, memory_symbol.type);
420 
421  if(base_type_eq(
422  ns.follow(memory_symbol.type).subtype(),
423  dereference_type, ns))
424  {
425  // Types match already, what a coincidence!
426  // We can use an index expression.
427 
428  const index_exprt index_expr(
429  symbol_expr,
430  pointer_offset(pointer_expr),
431  ns.follow(memory_symbol.type).subtype());
432  result.value=index_expr;
433  }
434  else if(dereference_type_compare(
435  ns.follow(memory_symbol.type).subtype(),
436  dereference_type))
437  {
438  const index_exprt index_expr(
439  symbol_expr,
440  pointer_offset(pointer_expr),
441  ns.follow(memory_symbol.type).subtype());
442  result.value=typecast_exprt(index_expr, dereference_type);
443  }
444  else
445  {
446  // We need to use byte_extract.
447  // Won't do this without a commitment to an endianness.
448 
450  {
451  }
452  else
453  {
454  result.value = byte_extract_exprt(
455  byte_extract_id(),
456  symbol_expr,
457  pointer_offset(pointer_expr),
458  dereference_type);
459  }
460  }
461  }
462  else
463  {
464  // something generic -- really has to be a symbol
465  address_of_exprt object_pointer(object);
466 
467  if(o.offset().is_zero())
468  {
469  equal_exprt equality(pointer_expr, object_pointer);
470 
471  if(ns.follow(equality.lhs().type())!=ns.follow(equality.rhs().type()))
472  equality.lhs().make_typecast(equality.rhs().type());
473 
474  result.pointer_guard=equality;
475  }
476  else
477  {
478  result.pointer_guard=same_object(pointer_expr, object_pointer);
479  }
480 
481  guardt tmp_guard(guard);
482  tmp_guard.add(result.pointer_guard);
483 
484  valid_check(object, tmp_guard, mode);
485 
486  const typet &object_type=ns.follow(object.type());
487  const exprt &root_object=o.root_object();
488  const typet &root_object_type=ns.follow(root_object.type());
489 
490  exprt root_object_subexpression=root_object;
491 
492  if(dereference_type_compare(object_type, dereference_type) &&
493  o.offset().is_zero())
494  {
495  // The simplest case: types match, and offset is zero!
496  // This is great, we are almost done.
497 
498  result.value=object;
499 
500  if(object_type!=ns.follow(dereference_type))
501  result.value.make_typecast(dereference_type);
502  }
503  else if(root_object_type.id()==ID_array &&
505  root_object_type.subtype(),
506  dereference_type))
507  {
508  // We have an array with a subtype that matches
509  // the dereferencing type.
510  // We will require well-alignedness!
511 
512  exprt offset;
513 
514  // this should work as the object is essentially the root object
515  if(o.offset().is_constant())
516  offset=o.offset();
517  else
518  offset=pointer_offset(pointer_expr);
519 
520  exprt adjusted_offset;
521 
522  // are we doing a byte?
523  mp_integer element_size =
524  pointer_offset_size(root_object_type.subtype(), ns);
525 
526  if(element_size==1)
527  {
528  // no need to adjust offset
529  adjusted_offset=offset;
530  }
531  else if(element_size<=0)
532  {
533  throw "unknown or invalid type size of:\n" +
534  root_object_type.subtype().pretty();
535  }
536  else
537  {
538  exprt element_size_expr=
539  from_integer(element_size, offset.type());
540 
541  adjusted_offset=binary_exprt(
542  offset, ID_div, element_size_expr, offset.type());
543 
544  // TODO: need to assert well-alignedness
545  }
546 
547  index_exprt index_expr=
548  index_exprt(root_object, adjusted_offset, root_object_type.subtype());
549 
550  bounds_check(index_expr, tmp_guard);
551 
552  result.value=index_expr;
553 
554  if(ns.follow(result.value.type())!=ns.follow(dereference_type))
555  result.value.make_typecast(dereference_type);
556  }
558  root_object_subexpression,
559  o.offset(),
560  dereference_type,
561  ns))
562  {
563  // Successfully found a member, array index, or combination thereof
564  // that matches the desired type and offset:
565  result.value=root_object_subexpression;
566  }
567  else
568  {
569  // we extract something from the root object
570  result.value=o.root_object();
571 
572  // this is relative to the root object
573  exprt offset;
574  if(o.offset().id()==ID_unknown)
575  offset=pointer_offset(pointer_expr);
576  else
577  offset=o.offset();
578 
579  if(memory_model(result.value, dereference_type, tmp_guard, offset))
580  {
581  // ok, done
582  }
583  else
584  {
585  if(options.get_bool_option("pointer-check"))
586  {
587  std::ostringstream msg;
588  msg << "memory model not applicable (got `"
589  << format(result.value.type()) << "', expected `"
590  << format(dereference_type) << "')";
591 
593  "pointer dereference", msg.str(), tmp_guard);
594  }
595 
596  return valuet(); // give up, no way that this is ok
597  }
598  }
599  }
600 
601  return result;
602 }
603 
605  const exprt &object,
606  const guardt &guard,
607  const modet mode)
608 {
609  if(!options.get_bool_option("pointer-check"))
610  return;
611 
612  const exprt &symbol_expr=get_symbol(object);
613 
614  if(symbol_expr.id()==ID_string_constant)
615  {
616  // always valid, but can't write
617 
618  if(mode==modet::WRITE)
619  {
621  "pointer dereference",
622  "write access to string constant",
623  guard);
624  }
625  }
626  else if(symbol_expr.is_nil() ||
627  symbol_expr.get_bool(ID_C_invalid_object))
628  {
629  // always "valid", shut up
630  return;
631  }
632  else if(symbol_expr.id()==ID_symbol)
633  {
634  const irep_idt identifier=
635  is_ssa_expr(symbol_expr)?
636  to_ssa_expr(symbol_expr).get_object_name():
637  to_symbol_expr(symbol_expr).get_identifier();
638 
639  const symbolt &symbol=ns.lookup(identifier);
640 
641  if(symbol.type.get_bool(ID_C_is_failed_symbol))
642  {
644  "pointer dereference",
645  "invalid pointer",
646  guard);
647  }
648 
649  #if 0
650  if(dereference_callback.is_valid_object(identifier))
651  return; // always ok
652  #endif
653  }
654 }
655 
657  const index_exprt &expr,
658  const guardt &guard)
659 {
660  if(!options.get_bool_option("pointer-check"))
661  return;
662 
663  if(!options.get_bool_option("bounds-check"))
664  return;
665 
666  const typet &array_type=ns.follow(expr.op0().type());
667 
668  if(array_type.id()!=ID_array)
669  throw "bounds check expected array type";
670 
671  std::string name=array_name(ns, expr.array());
672 
673  {
674  mp_integer i;
675  if(!to_integer(expr.index(), i) &&
676  i>=0)
677  {
678  }
679  else
680  {
681  exprt zero=from_integer(0, expr.index().type());
682 
683  if(zero.is_nil())
684  throw "no zero constant of index type "+
685  expr.index().type().pretty();
686 
688  inequality(expr.index(), ID_lt, zero);
689 
690  guardt tmp_guard(guard);
691  tmp_guard.add(inequality);
693  "array bounds",
694  name+" lower bound", tmp_guard);
695  }
696  }
697 
698  const exprt &size_expr=
699  to_array_type(array_type).size();
700 
701  if(size_expr.id()==ID_infinity)
702  {
703  }
704  else if(size_expr.is_zero() && expr.array().id()==ID_member)
705  {
706  // this is a variable-sized struct field
707  }
708  else
709  {
710  if(size_expr.is_nil())
711  throw "index array operand of wrong type";
712 
713  binary_relation_exprt inequality(
714  typecast_exprt::conditional_cast(expr.index(), size_expr.type()),
715  ID_ge,
716  size_expr);
717 
718  guardt tmp_guard(guard);
719  tmp_guard.add(inequality);
721  "array bounds",
722  name+" upper bound", tmp_guard);
723  }
724 }
725 
726 static bool is_a_bv_type(const typet &type)
727 {
728  return type.id()==ID_unsignedbv ||
729  type.id()==ID_signedbv ||
730  type.id()==ID_bv ||
731  type.id()==ID_fixedbv ||
732  type.id()==ID_floatbv ||
733  type.id()==ID_c_enum_tag;
734 }
735 
737  exprt &value,
738  const typet &to_type,
739  const guardt &guard,
740  const exprt &offset)
741 {
742  // we will allow more or less arbitrary pointer type cast
743 
744  const typet from_type=value.type();
745 
746  // first, check if it's really just a type coercion,
747  // i.e., both have exactly the same (constant) size
748 
749  if(is_a_bv_type(from_type) &&
750  is_a_bv_type(to_type))
751  {
753  {
754  // avoid semantic conversion in case of
755  // cast to float or fixed-point,
756  // or cast from float or fixed-point
757 
758  if(to_type.id()==ID_fixedbv || to_type.id()==ID_floatbv ||
759  from_type.id()==ID_fixedbv || from_type.id()==ID_floatbv)
760  {
761  }
762  else
763  return memory_model_conversion(value, to_type, guard, offset);
764  }
765  }
766 
767  // we are willing to do the same for pointers
768 
769  if(from_type.id()==ID_pointer &&
770  to_type.id()==ID_pointer)
771  {
773  return memory_model_conversion(value, to_type, guard, offset);
774  }
775 
776  // otherwise, we will stitch it together from bytes
777 
778  return memory_model_bytes(value, to_type, guard, offset);
779 }
780 
782  exprt &value,
783  const typet &to_type,
784  const guardt &guard,
785  const exprt &offset)
786 {
787  // only doing type conversion
788  // just do the typecast
789  value.make_typecast(to_type);
790 
791  // also assert that offset is zero
792 
793  if(options.get_bool_option("pointer-check"))
794  {
795  equal_exprt offset_not_zero(offset, from_integer(0, offset.type()));
796  offset_not_zero.make_not();
797 
798  guardt tmp_guard(guard);
799  tmp_guard.add(offset_not_zero);
801  "word bounds",
802  "offset not zero", tmp_guard);
803  }
804 
805  return true;
806 }
807 
809  exprt &value,
810  const typet &to_type,
811  const guardt &guard,
812  const exprt &offset)
813 {
814  const typet from_type=value.type();
815 
816  // We simply refuse to convert to/from code.
817  if(from_type.id()==ID_code || to_type.id()==ID_code)
818  return false;
819 
820  // We won't do this without a commitment to an endianness.
822  return false;
823 
824  // But everything else we will try!
825  // We just rely on byte_extract to do the job!
826 
827  exprt result;
828 
829  // See if we have an array of bytes already,
830  // and we want something byte-sized.
831  if(ns.follow(from_type).id()==ID_array &&
833  pointer_offset_size(to_type, ns)==1 &&
835  is_a_bv_type(to_type))
836  {
837  // yes, can use 'index'
838  result=index_exprt(value, offset, ns.follow(from_type).subtype());
839 
840  // possibly need to convert
841  if(!base_type_eq(result.type(), to_type, ns))
842  result.make_typecast(to_type);
843  }
844  else
845  {
846  // no, use 'byte_extract'
847  result = byte_extract_exprt(byte_extract_id(), value, offset, to_type);
848  }
849 
850  value=result;
851 
852  // are we within the bounds?
853  if(options.get_bool_option("pointer-check"))
854  {
855  // upper bound
856  {
857  exprt from_width=size_of_expr(from_type, ns);
858  INVARIANT(
859  from_width.is_not_nil(),
860  "unknown or invalid type size:\n"+from_type.pretty());
861 
862  exprt to_width=
863  to_type.id()==ID_empty?
864  from_integer(0, size_type()):size_of_expr(to_type, ns);
865  INVARIANT(
866  to_width.is_not_nil(),
867  "unknown or invalid type size:\n"+to_type.pretty());
868  INVARIANT(
869  from_width.type()==to_width.type(),
870  "type mismatch on result of size_of_expr");
871 
872  minus_exprt bound(from_width, to_width);
873  if(bound.type()!=offset.type())
874  bound.make_typecast(offset.type());
875 
877  offset_upper_bound(offset, ID_gt, bound);
878 
879  guardt tmp_guard(guard);
880  tmp_guard.add(offset_upper_bound);
882  "pointer dereference",
883  "object upper bound", tmp_guard);
884  }
885 
886  // lower bound is easy
887  if(!offset.is_zero())
888  {
890  offset_lower_bound(
891  offset, ID_lt, from_integer(0, offset.type()));
892 
893  guardt tmp_guard(guard);
894  tmp_guard.add(offset_lower_bound);
896  "pointer dereference",
897  "object lower bound", tmp_guard);
898  }
899  }
900 
901  return true;
902 }
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
Definition: std_expr.h:3426
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:3230
exprt & true_case()
Definition: std_expr.h:3395
semantic type conversion
Definition: std_expr.h:2111
BigInt mp_integer
Definition: mp_arith.h:22
bool is_nil() const
Definition: irep.h:102
A generic base class for relations, i.e., binary predicates.
Definition: std_expr.h:752
bool is_not_nil() const
Definition: irep.h:103
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:1150
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:3361
exprt & cond()
Definition: std_expr.h:3385
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)
#define INVARIANT(CONDITION, REASON)
Definition: invariant.h:205
equality
Definition: std_expr.h:1354
const irep_idt & id() const
Definition: irep.h:189
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:4488
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:4510
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:3284
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:1014
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
valuet build_reference_to(const exprt &what, const modet mode, const exprt &pointer, const guardt &guard)
Operator to return the address of an object.
Definition: std_expr.h:3170
exprt & false_case()
Definition: std_expr.h:3405
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:1129
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 dynamic_object_upper_bound(const exprt &pointer, const typet &dereference_type, const namespacet &ns, const exprt &access_size)
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:1045
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:192
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:130
void add(const exprt &expr)
Definition: guard.cpp:64
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:214
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
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