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