cprover
value_set_fi.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Value Set (Flow Insensitive, Sharing)
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "value_set_fi.h"
13 
14 #include <cassert>
15 #include <ostream>
16 
17 #include <util/symbol_table.h>
18 #include <util/simplify_expr.h>
19 #include <util/base_type.h>
20 #include <util/std_expr.h>
21 #include <util/prefix.h>
22 #include <util/std_code.h>
23 #include <util/arith_tools.h>
24 
25 #include <langapi/language_util.h>
26 #include <util/c_types.h>
27 
29 
32 
33 static const char *alloc_adapter_prefix="alloc_adaptor::";
34 
35 #define forall_objects(it, map) \
36  for(object_map_dt::const_iterator it = (map).begin(); \
37  it!=(map).end(); \
38  (it)++)
39 
40 #define Forall_objects(it, map) \
41  for(object_map_dt::iterator it = (map).begin(); \
42  it!=(map).end(); \
43  (it)++)
44 
46  const namespacet &ns,
47  std::ostream &out) const
48 {
49  for(valuest::const_iterator
50  v_it=values.begin();
51  v_it!=values.end();
52  v_it++)
53  {
54  irep_idt identifier, display_name;
55 
56  const entryt &e=v_it->second;
57 
58  if(has_prefix(id2string(e.identifier), "value_set::dynamic_object"))
59  {
60  display_name=id2string(e.identifier)+e.suffix;
61  identifier="";
62  }
63  else
64  {
65  #if 0
66  const symbolt &symbol=ns.lookup(id2string(e.identifier));
67  display_name=symbol.display_name()+e.suffix;
68  identifier=symbol.name;
69  #else
70  identifier=id2string(e.identifier);
71  display_name=id2string(identifier)+e.suffix;
72  #endif
73  }
74 
75  out << display_name;
76 
77  out << " = { ";
78 
79  object_mapt object_map;
80  flatten(e, object_map);
81 
82  std::size_t width=0;
83 
84  forall_objects(o_it, object_map.read())
85  {
86  const exprt &o=object_numbering[o_it->first];
87 
88  std::string result;
89 
90  if(o.id()==ID_invalid || o.id()==ID_unknown)
91  {
92  result="<";
93  result+=from_expr(ns, identifier, o);
94  result+=", *, "; // offset unknown
95  if(o.type().id()==ID_unknown)
96  result+='*';
97  else
98  result+=from_type(ns, identifier, o.type());
99  result+='>';
100  }
101  else
102  {
103  result="<"+from_expr(ns, identifier, o)+", ";
104 
105  if(o_it->second)
106  result += integer2string(*o_it->second) + "";
107  else
108  result+='*';
109 
110  result+=", ";
111 
112  if(o.type().id()==ID_unknown)
113  result+='*';
114  else
115  result+=from_type(ns, identifier, o.type());
116 
117  result+='>';
118  }
119 
120  out << result;
121 
122  width+=result.size();
123 
125  next++;
126 
127  if(next!=object_map.read().end())
128  {
129  out << ", ";
130  if(width>=40)
131  out << "\n ";
132  }
133  }
134 
135  out << " } \n";
136  }
137 }
138 
140  const entryt &e,
141  object_mapt &dest) const
142 {
143  #if 0
144  std::cout << "FLATTEN: " << e.identifier << e.suffix << '\n';
145  #endif
146 
147  flatten_seent seen;
148  flatten_rec(e, dest, seen);
149 
150  #if 0
151  std::cout << "FLATTEN: Done.\n";
152  #endif
153 }
154 
156  const entryt &e,
157  object_mapt &dest,
158  flatten_seent &seen) const
159 {
160  #if 0
161  std::cout << "FLATTEN_REC: " << e.identifier << e.suffix << '\n';
162  #endif
163 
164  std::string identifier = id2string(e.identifier);
165  assert(seen.find(identifier + e.suffix)==seen.end());
166 
167  bool generalize_index = false;
168 
169  seen.insert(identifier + e.suffix);
170 
172  {
173  const exprt &o=object_numbering[it->first];
174 
175  if(o.type().id()=="#REF#")
176  {
177  if(seen.find(o.get(ID_identifier))!=seen.end())
178  {
179  generalize_index = true;
180  continue;
181  }
182 
183  valuest::const_iterator fi = values.find(o.get(ID_identifier));
184  if(fi==values.end())
185  {
186  // this is some static object, keep it in.
187  const symbol_exprt se(o.get(ID_identifier), o.type().subtype());
188  insert(dest, se, 0);
189  }
190  else
191  {
192  object_mapt temp;
193  flatten_rec(fi->second, temp, seen);
194 
195  for(object_map_dt::iterator t_it=temp.write().begin();
196  t_it!=temp.write().end();
197  t_it++)
198  {
199  if(t_it->second && it->second)
200  {
201  *t_it->second += *it->second;
202  }
203  else
204  t_it->second.reset();
205  }
206 
207  forall_objects(oit, temp.read())
208  insert(dest, *oit);
209  }
210  }
211  else
212  insert(dest, *it);
213  }
214 
215  if(generalize_index) // this means we had recursive symbols in there
216  {
217  Forall_objects(it, dest.write())
218  it->second.reset();
219  }
220 
221  seen.erase(identifier + e.suffix);
222 }
223 
225 {
226  const exprt &object=object_numbering[it.first];
227 
228  if(object.id()==ID_invalid ||
229  object.id()==ID_unknown)
230  return object;
231 
233 
234  od.object()=object;
235 
236  if(it.second)
237  od.offset() = from_integer(*it.second, index_type());
238 
239  od.type()=od.object().type();
240 
241  return od;
242 }
243 
245 {
246  UNREACHABLE;
247  bool result=false;
248 
249  for(valuest::const_iterator
250  it=new_values.begin();
251  it!=new_values.end();
252  it++)
253  {
254  valuest::iterator it2=values.find(it->first);
255 
256  if(it2==values.end())
257  {
258  // we always track these
259  if(has_prefix(id2string(it->second.identifier),
260  "value_set::dynamic_object") ||
261  has_prefix(id2string(it->second.identifier),
262  "value_set::return_value"))
263  {
264  values.insert(*it);
265  result=true;
266  }
267 
268  continue;
269  }
270 
271  entryt &e=it2->second;
272  const entryt &new_e=it->second;
273 
274  if(make_union(e.object_map, new_e.object_map))
275  result=true;
276  }
277 
278  changed = result;
279 
280  return result;
281 }
282 
283 bool value_set_fit::make_union(object_mapt &dest, const object_mapt &src) const
284 {
285  bool result=false;
286 
287  forall_objects(it, src.read())
288  {
289  if(insert(dest, *it))
290  result=true;
291  }
292 
293  return result;
294 }
295 
297  const exprt &expr,
298  std::list<exprt> &value_set,
299  const namespacet &ns) const
300 {
301  object_mapt object_map;
302  get_value_set(expr, object_map, ns);
303 
304  object_mapt flat_map;
305 
306  forall_objects(it, object_map.read())
307  {
308  const exprt &object=object_numbering[it->first];
309  if(object.type().id()=="#REF#")
310  {
311  assert(object.id()==ID_symbol);
312 
313  const irep_idt &ident = object.get(ID_identifier);
314  valuest::const_iterator v_it = values.find(ident);
315 
316  if(v_it!=values.end())
317  {
318  object_mapt temp;
319  flatten(v_it->second, temp);
320 
321  for(object_map_dt::iterator t_it=temp.write().begin();
322  t_it!=temp.write().end();
323  t_it++)
324  {
325  if(t_it->second && it->second)
326  {
327  *t_it->second += *it->second;
328  }
329  else
330  t_it->second.reset();
331 
332  flat_map.write()[t_it->first]=t_it->second;
333  }
334  }
335  }
336  else
337  flat_map.write()[it->first]=it->second;
338  }
339 
340  forall_objects(fit, flat_map.read())
341  value_set.push_back(to_expr(*fit));
342 
343  #if 0
344  // Sanity check!
345  for(std::list<exprt>::const_iterator it=value_set.begin();
346  it!=value_set.end();
347  it++)
348  assert(it->type().id()!="#REF");
349  #endif
350 
351  #if 0
352  for(expr_sett::const_iterator it=value_set.begin(); it!=value_set.end(); it++)
353  std::cout << "GET_VALUE_SET: " << format(*it) << '\n';
354  #endif
355 }
356 
358  const exprt &expr,
359  object_mapt &dest,
360  const namespacet &ns) const
361 {
362  exprt tmp(expr);
363  simplify(tmp, ns);
364 
365  gvs_recursion_sett recset;
366  get_value_set_rec(tmp, dest, "", tmp.type(), ns, recset);
367 }
368 
370  const exprt &expr,
371  object_mapt &dest,
372  const std::string &suffix,
373  const typet &original_type,
374  const namespacet &ns,
375  gvs_recursion_sett &recursion_set) const
376 {
377  #if 0
378  std::cout << "GET_VALUE_SET_REC EXPR: " << format(expr)
379  << '\n';
380  std::cout << "GET_VALUE_SET_REC SUFFIX: " << suffix << '\n';
381  std::cout << '\n';
382  #endif
383 
384  if(expr.type().id()=="#REF#")
385  {
386  valuest::const_iterator fi = values.find(expr.get(ID_identifier));
387 
388  if(fi!=values.end())
389  {
390  forall_objects(it, fi->second.object_map.read())
391  get_value_set_rec(object_numbering[it->first], dest, suffix,
392  original_type, ns, recursion_set);
393  return;
394  }
395  else
396  {
397  insert(dest, exprt(ID_unknown, original_type));
398  return;
399  }
400  }
401  else if(expr.id()==ID_unknown || expr.id()==ID_invalid)
402  {
403  insert(dest, exprt(ID_unknown, original_type));
404  return;
405  }
406  else if(expr.id()==ID_index)
407  {
408  assert(expr.operands().size()==2);
409 
410  const typet &type=ns.follow(expr.op0().type());
411 
412  DATA_INVARIANT(type.id()==ID_array ||
413  type.id()==ID_incomplete_array ||
414  type.id()=="#REF#",
415  "operand 0 of index expression must be an array");
416 
417  get_value_set_rec(expr.op0(), dest, "[]"+suffix,
418  original_type, ns, recursion_set);
419 
420  return;
421  }
422  else if(expr.id()==ID_member)
423  {
424  assert(expr.operands().size()==1);
425 
426  if(expr.op0().is_not_nil())
427  {
428  const typet &type=ns.follow(expr.op0().type());
429 
430  DATA_INVARIANT(type.id()==ID_struct ||
431  type.id()==ID_union ||
432  type.id()==ID_incomplete_struct ||
433  type.id()==ID_incomplete_union,
434  "operand 0 of member expression must be struct or union");
435 
436  const std::string &component_name=
437  expr.get_string(ID_component_name);
438 
439  get_value_set_rec(expr.op0(), dest, "."+component_name+suffix,
440  original_type, ns, recursion_set);
441 
442  return;
443  }
444  }
445  else if(expr.id()==ID_symbol)
446  {
447  // just keep a reference to the ident in the set
448  // (if it exists)
449  irep_idt ident = id2string(to_symbol_expr(expr).get_identifier()) + suffix;
450  valuest::const_iterator v_it=values.find(ident);
451 
453  {
454  insert(dest, expr, 0);
455  return;
456  }
457  else if(v_it!=values.end())
458  {
459  typet t("#REF#");
460  t.subtype() = expr.type();
461  symbol_exprt sym(ident, t);
462  insert(dest, sym, 0);
463  return;
464  }
465  }
466  else if(expr.id()==ID_if)
467  {
468  if(expr.operands().size()!=3)
469  throw "if takes three operands";
470 
471  get_value_set_rec(expr.op1(), dest, suffix,
472  original_type, ns, recursion_set);
473  get_value_set_rec(expr.op2(), dest, suffix,
474  original_type, ns, recursion_set);
475 
476  return;
477  }
478  else if(expr.id()==ID_address_of)
479  {
480  if(expr.operands().size()!=1)
481  throw expr.id_string()+" expected to have one operand";
482 
483  get_reference_set_sharing(expr.op0(), dest, ns);
484 
485  return;
486  }
487  else if(expr.id()==ID_dereference)
488  {
489  object_mapt reference_set;
490  get_reference_set_sharing(expr, reference_set, ns);
491  const object_map_dt &object_map=reference_set.read();
492 
493  if(object_map.begin()!=object_map.end())
494  {
495  forall_objects(it1, object_map)
496  {
497  const exprt &object=object_numbering[it1->first];
498  get_value_set_rec(object, dest, suffix,
499  original_type, ns, recursion_set);
500  }
501 
502  return;
503  }
504  }
505  else if(expr.id()=="reference_to")
506  {
507  object_mapt reference_set;
508 
509  get_reference_set_sharing(expr, reference_set, ns);
510 
511  const object_map_dt &object_map=reference_set.read();
512 
513  if(object_map.begin()!=object_map.end())
514  {
515  forall_objects(it, object_map)
516  {
517  const exprt &object=object_numbering[it->first];
518  get_value_set_rec(object, dest, suffix,
519  original_type, ns, recursion_set);
520  }
521 
522  return;
523  }
524  }
525  else if(expr.is_constant())
526  {
527  // check if NULL
528  if(expr.get(ID_value)==ID_NULL &&
529  expr.type().id()==ID_pointer)
530  {
531  insert(dest, exprt(ID_null_object, expr.type().subtype()), 0);
532  return;
533  }
534  }
535  else if(expr.id()==ID_typecast)
536  {
537  if(expr.operands().size()!=1)
538  throw "typecast takes one operand";
539 
540  get_value_set_rec(expr.op0(), dest, suffix,
541  original_type, ns, recursion_set);
542 
543  return;
544  }
545  else if(expr.id()==ID_plus || expr.id()==ID_minus)
546  {
547  if(expr.operands().size()<2)
548  throw expr.id_string()+" expected to have at least two operands";
549 
550  if(expr.type().id()==ID_pointer)
551  {
552  // find the pointer operand
553  const exprt *ptr_operand=nullptr;
554 
555  forall_operands(it, expr)
556  if(it->type().id()==ID_pointer)
557  {
558  if(ptr_operand==nullptr)
559  ptr_operand=&(*it);
560  else
561  throw "more than one pointer operand in pointer arithmetic";
562  }
563 
564  if(ptr_operand==nullptr)
565  throw "pointer type sum expected to have pointer operand";
566 
567  object_mapt pointer_expr_set;
568  get_value_set_rec(*ptr_operand, pointer_expr_set, "",
569  ptr_operand->type(), ns, recursion_set);
570 
571  forall_objects(it, pointer_expr_set.read())
572  {
573  offsett offset = it->second;
574 
575  if(offset_is_zero(offset) && expr.operands().size() == 2)
576  {
577  if(expr.op0().type().id()!=ID_pointer)
578  {
579  mp_integer i;
580  if(to_integer(expr.op0(), i))
581  offset.reset();
582  else
583  *offset = (expr.id() == ID_plus) ? i : -i;
584  }
585  else
586  {
587  mp_integer i;
588  if(to_integer(expr.op1(), i))
589  offset.reset();
590  else
591  *offset = (expr.id() == ID_plus) ? i : -i;
592  }
593  }
594  else
595  offset.reset();
596 
597  insert(dest, it->first, offset);
598  }
599 
600  return;
601  }
602  }
603  else if(expr.id()==ID_side_effect)
604  {
605  const irep_idt &statement=expr.get(ID_statement);
606 
607  if(statement==ID_function_call)
608  {
609  // these should be gone
610  throw "unexpected function_call sideeffect";
611  }
612  else if(statement==ID_allocate)
613  {
614  if(expr.type().id()!=ID_pointer)
615  throw "malloc expected to return pointer type";
616 
617  assert(suffix=="");
618 
619  const typet &dynamic_type=
620  static_cast<const typet &>(expr.find(ID_C_cxx_alloc_type));
621 
622  dynamic_object_exprt dynamic_object(dynamic_type);
623  // let's make up a `unique' number for this object...
624  dynamic_object.set_instance(
625  (from_function << 16) | from_target_index);
626  dynamic_object.valid()=true_exprt();
627 
628  insert(dest, dynamic_object, 0);
629  return;
630  }
631  else if(statement==ID_cpp_new ||
632  statement==ID_cpp_new_array)
633  {
634  assert(suffix=="");
635  assert(expr.type().id()==ID_pointer);
636 
638  dynamic_object.set_instance(
639  (from_function << 16) | from_target_index);
640  dynamic_object.valid()=true_exprt();
641 
642  insert(dest, dynamic_object, 0);
643  return;
644  }
645  }
646  else if(expr.id()==ID_struct)
647  {
648  // this is like a static struct object
649  insert(dest, address_of_exprt(expr), 0);
650  return;
651  }
652  else if(expr.id()==ID_with)
653  {
654  // these are supposed to be done by assign()
655  throw "unexpected value in get_value_set: "+expr.id_string();
656  }
657  else if(expr.id()==ID_array_of ||
658  expr.id()==ID_array)
659  {
660  // an array constructor, possibly containing addresses
661  forall_operands(it, expr)
662  get_value_set_rec(*it, dest, suffix, original_type, ns, recursion_set);
663  }
664  else if(expr.id()==ID_dynamic_object)
665  {
668 
669  const std::string name=
670  "value_set::dynamic_object"+
671  std::to_string(dynamic_object.get_instance())+
672  suffix;
673 
674  // look it up
675  valuest::const_iterator v_it=values.find(name);
676 
677  if(v_it!=values.end())
678  {
679  make_union(dest, v_it->second.object_map);
680  return;
681  }
682  }
683 
684  insert(dest, exprt(ID_unknown, original_type));
685 }
686 
688  const exprt &src,
689  exprt &dest) const
690 {
691  // remove pointer typecasts
692  if(src.id()==ID_typecast)
693  {
694  assert(src.type().id()==ID_pointer);
695 
696  if(src.operands().size()!=1)
697  throw "typecast expects one operand";
698 
699  dereference_rec(src.op0(), dest);
700  }
701  else
702  dest=src;
703 }
704 
706  const exprt &expr,
707  expr_sett &dest,
708  const namespacet &ns) const
709 {
710  object_mapt object_map;
711  get_reference_set_sharing(expr, object_map, ns);
712 
713  forall_objects(it, object_map.read())
714  {
715  const exprt &expr = object_numbering[it->first];
716 
717  if(expr.type().id()=="#REF#")
718  {
719  const irep_idt &ident = expr.get(ID_identifier);
720  valuest::const_iterator vit = values.find(ident);
721  if(vit==values.end())
722  {
723  // Assume the variable never was assigned,
724  // so assume it's reference set is unknown.
725  dest.insert(exprt(ID_unknown, expr.type()));
726  }
727  else
728  {
729  object_mapt omt;
730  flatten(vit->second, omt);
731 
732  for(object_map_dt::iterator t_it=omt.write().begin();
733  t_it!=omt.write().end();
734  t_it++)
735  {
736  if(t_it->second && it->second)
737  {
738  *t_it->second += *it->second;
739  }
740  else
741  t_it->second.reset();
742  }
743 
744  forall_objects(it, omt.read())
745  dest.insert(to_expr(*it));
746  }
747  }
748  else
749  dest.insert(to_expr(*it));
750  }
751 }
752 
754  const exprt &expr,
755  expr_sett &dest,
756  const namespacet &ns) const
757 {
758  object_mapt object_map;
759  get_reference_set_sharing(expr, object_map, ns);
760 
761  forall_objects(it, object_map.read())
762  dest.insert(to_expr(*it));
763 }
764 
766  const exprt &expr,
767  object_mapt &dest,
768  const namespacet &ns) const
769 {
770  #if 0
771  std::cout << "GET_REFERENCE_SET_REC EXPR: " << format(expr)
772  << '\n';
773  #endif
774 
775  if(expr.type().id()=="#REF#")
776  {
777  valuest::const_iterator fi = values.find(expr.get(ID_identifier));
778  if(fi!=values.end())
779  {
780  forall_objects(it, fi->second.object_map.read())
781  get_reference_set_sharing_rec(object_numbering[it->first], dest, ns);
782  return;
783  }
784  }
785  else if(expr.id()==ID_symbol ||
786  expr.id()==ID_dynamic_object ||
787  expr.id()==ID_string_constant)
788  {
789  if(expr.type().id()==ID_array &&
790  expr.type().subtype().id()==ID_array)
791  insert(dest, expr);
792  else
793  insert(dest, expr, 0);
794 
795  return;
796  }
797  else if(expr.id()==ID_dereference)
798  {
799  if(expr.operands().size()!=1)
800  throw expr.id_string()+" expected to have one operand";
801 
802  gvs_recursion_sett recset;
803  object_mapt temp;
804  get_value_set_rec(expr.op0(), temp, "", expr.op0().type(), ns, recset);
805 
806  // REF's need to be dereferenced manually!
807  forall_objects(it, temp.read())
808  {
809  const exprt &obj = object_numbering[it->first];
810  if(obj.type().id()=="#REF#")
811  {
812  const irep_idt &ident = obj.get(ID_identifier);
813  valuest::const_iterator v_it = values.find(ident);
814 
815  if(v_it!=values.end())
816  {
817  object_mapt t2;
818  flatten(v_it->second, t2);
819 
820  for(object_map_dt::iterator t_it=t2.write().begin();
821  t_it!=t2.write().end();
822  t_it++)
823  {
824  if(t_it->second && it->second)
825  {
826  *t_it->second += *it->second;
827  }
828  else
829  t_it->second.reset();
830  }
831 
832  forall_objects(it2, t2.read())
833  insert(dest, *it2);
834  }
835  else
836  insert(dest, exprt(ID_unknown, obj.type().subtype()));
837  }
838  else
839  insert(dest, *it);
840  }
841 
842  #if 0
843  for(expr_sett::const_iterator it=value_set.begin();
844  it!=value_set.end();
845  it++)
846  std::cout << "VALUE_SET: " << format(*it) << '\n';
847  #endif
848 
849  return;
850  }
851  else if(expr.id()==ID_index)
852  {
853  if(expr.operands().size()!=2)
854  throw "index expected to have two operands";
855 
856  const exprt &array=expr.op0();
857  const exprt &offset=expr.op1();
858  const typet &array_type=ns.follow(array.type());
859 
860  assert(array_type.id()==ID_array ||
861  array_type.id()==ID_incomplete_array);
862 
863  object_mapt array_references;
864  get_reference_set_sharing(array, array_references, ns);
865 
866  const object_map_dt &object_map=array_references.read();
867 
868  forall_objects(a_it, object_map)
869  {
870  const exprt &object=object_numbering[a_it->first];
871 
872  if(object.id()==ID_unknown)
873  insert(dest, exprt(ID_unknown, expr.type()));
874  else
875  {
876  index_exprt index_expr(
877  object, from_integer(0, index_type()), expr.type());
878 
879  // adjust type?
880  if(object.type().id()!="#REF#" &&
881  ns.follow(object.type())!=array_type)
882  index_expr.make_typecast(array.type());
883 
884  offsett o = a_it->second;
885  mp_integer i;
886 
887  if(offset.is_zero())
888  {
889  }
890  else if(!to_integer(offset, i) && offset_is_zero(o))
891  *o = i;
892  else
893  o.reset();
894 
895  insert(dest, index_expr, o);
896  }
897  }
898 
899  return;
900  }
901  else if(expr.id()==ID_member)
902  {
903  const irep_idt &component_name=expr.get(ID_component_name);
904 
905  if(expr.operands().size()!=1)
906  throw "member expected to have one operand";
907 
908  const exprt &struct_op=expr.op0();
909 
910  object_mapt struct_references;
911  get_reference_set_sharing(struct_op, struct_references, ns);
912 
913  forall_objects(it, struct_references.read())
914  {
915  const exprt &object=object_numbering[it->first];
916  const typet &obj_type=ns.follow(object.type());
917 
918  if(object.id()==ID_unknown)
919  insert(dest, exprt(ID_unknown, expr.type()));
920  else if(object.id()==ID_dynamic_object &&
921  obj_type.id()!=ID_struct &&
922  obj_type.id()!=ID_union)
923  {
924  // we catch dynamic objects of the wrong type,
925  // to avoid non-integral typecasts.
926  insert(dest, exprt(ID_unknown, expr.type()));
927  }
928  else
929  {
930  offsett o = it->second;
931 
932  member_exprt member_expr(object, component_name, expr.type());
933 
934  // adjust type?
935  if(ns.follow(struct_op.type())!=ns.follow(object.type()))
936  member_expr.op0().make_typecast(struct_op.type());
937 
938  insert(dest, member_expr, o);
939  }
940  }
941 
942  return;
943  }
944  else if(expr.id()==ID_if)
945  {
946  if(expr.operands().size()!=3)
947  throw "if takes three operands";
948 
949  get_reference_set_sharing_rec(expr.op1(), dest, ns);
950  get_reference_set_sharing_rec(expr.op2(), dest, ns);
951  return;
952  }
953 
954  insert(dest, exprt(ID_unknown, expr.type()));
955 }
956 
958  const exprt &lhs,
959  const exprt &rhs,
960  const namespacet &ns)
961 {
962  #if 0
963  std::cout << "ASSIGN LHS: " << format(lhs) << '\n';
964  std::cout << "ASSIGN RHS: " << format(rhs) << '\n';
965  #endif
966 
967  if(rhs.id()==ID_if)
968  {
969  if(rhs.operands().size()!=3)
970  throw "if takes three operands";
971 
972  assign(lhs, rhs.op1(), ns);
973  assign(lhs, rhs.op2(), ns);
974  return;
975  }
976 
977  const typet &type=ns.follow(lhs.type());
978 
979  if(type.id()==ID_struct ||
980  type.id()==ID_union)
981  {
982  const struct_union_typet &struct_type=to_struct_union_type(type);
983 
984  std::size_t no=0;
985 
986  for(struct_typet::componentst::const_iterator
987  c_it=struct_type.components().begin();
988  c_it!=struct_type.components().end();
989  c_it++, no++)
990  {
991  const typet &subtype=c_it->type();
992  const irep_idt &name=c_it->get(ID_name);
993 
994  // ignore methods
995  if(subtype.id()==ID_code)
996  continue;
997 
998  member_exprt lhs_member(lhs, name, subtype);
999 
1000  exprt rhs_member;
1001 
1002  if(rhs.id()==ID_unknown ||
1003  rhs.id()==ID_invalid)
1004  {
1005  rhs_member=exprt(rhs.id(), subtype);
1006  }
1007  else
1008  {
1009  if(!base_type_eq(rhs.type(), type, ns))
1010  throw "value_set_fit::assign type mismatch: "
1011  "rhs.type():\n"+rhs.type().pretty()+"\n"+
1012  "type:\n"+type.pretty();
1013 
1014  if(rhs.id()==ID_struct ||
1015  rhs.id()==ID_constant)
1016  {
1017  assert(no<rhs.operands().size());
1018  rhs_member=rhs.operands()[no];
1019  }
1020  else if(rhs.id()==ID_with)
1021  {
1022  assert(rhs.operands().size()==3);
1023 
1024  // see if op1 is the member we want
1025  const exprt &member_operand=rhs.op1();
1026 
1027  const irep_idt &component_name=
1028  member_operand.get(ID_component_name);
1029 
1030  if(component_name==name)
1031  {
1032  // yes! just take op2
1033  rhs_member=rhs.op2();
1034  }
1035  else
1036  {
1037  // no! do op0
1038  rhs_member=exprt(ID_member, subtype);
1039  rhs_member.copy_to_operands(rhs.op0());
1040  rhs_member.set(ID_component_name, name);
1041  }
1042  }
1043  else
1044  {
1045  rhs_member=exprt(ID_member, subtype);
1046  rhs_member.copy_to_operands(rhs);
1047  rhs_member.set(ID_component_name, name);
1048  }
1049 
1050  assign(lhs_member, rhs_member, ns);
1051  }
1052  }
1053  }
1054  else if(type.id()==ID_array)
1055  {
1056  const index_exprt lhs_index(
1057  lhs, exprt(ID_unknown, index_type()), type.subtype());
1058 
1059  if(rhs.id()==ID_unknown ||
1060  rhs.id()==ID_invalid)
1061  {
1062  assign(lhs_index, exprt(rhs.id(), type.subtype()), ns);
1063  }
1064  else if(rhs.is_nil())
1065  {
1066  // do nothing
1067  }
1068  else
1069  {
1070  if(!base_type_eq(rhs.type(), type, ns))
1071  throw "value_set_fit::assign type mismatch: "
1072  "rhs.type():\n"+rhs.type().pretty()+"\n"+
1073  "type:\n"+type.pretty();
1074 
1075  if(rhs.id()==ID_array_of)
1076  {
1077  assert(rhs.operands().size()==1);
1078  assign(lhs_index, rhs.op0(), ns);
1079  }
1080  else if(rhs.id()==ID_array ||
1081  rhs.id()==ID_constant)
1082  {
1083  forall_operands(o_it, rhs)
1084  {
1085  assign(lhs_index, *o_it, ns);
1086  }
1087  }
1088  else if(rhs.id()==ID_with)
1089  {
1090  assert(rhs.operands().size()==3);
1091 
1092  const index_exprt op0_index(
1093  rhs.op0(), exprt(ID_unknown, index_type()), type.subtype());
1094 
1095  assign(lhs_index, op0_index, ns);
1096  assign(lhs_index, rhs.op2(), ns);
1097  }
1098  else
1099  {
1100  const index_exprt rhs_index(
1101  rhs, exprt(ID_unknown, index_type()), type.subtype());
1102  assign(lhs_index, rhs_index, ns);
1103  }
1104  }
1105  }
1106  else
1107  {
1108  // basic type
1109  object_mapt values_rhs;
1110 
1111  get_value_set(rhs, values_rhs, ns);
1112 
1113  assign_recursion_sett recset;
1114  assign_rec(lhs, values_rhs, "", ns, recset);
1115  }
1116 }
1117 
1119  const exprt &op,
1120  const namespacet &ns)
1121 {
1122  // op must be a pointer
1123  if(op.type().id()!=ID_pointer)
1124  throw "free expected to have pointer-type operand";
1125 
1126  // find out what it points to
1127  object_mapt value_set;
1128  get_value_set(op, value_set, ns);
1129  entryt e; e.identifier="VP:TEMP";
1130  e.object_map = value_set;
1131  flatten(e, value_set);
1132 
1133  const object_map_dt &object_map=value_set.read();
1134 
1135  // find out which *instances* interest us
1136  dynamic_object_id_sett to_mark;
1137 
1138  forall_objects(it, object_map)
1139  {
1140  const exprt &object=object_numbering[it->first];
1141 
1142  if(object.id()==ID_dynamic_object)
1143  {
1145  to_dynamic_object_expr(object);
1146 
1147  if(dynamic_object.valid().is_true())
1148  to_mark.insert(dynamic_object.get_instance());
1149  }
1150  }
1151 
1152  // mark these as 'may be invalid'
1153  // this, unfortunately, destroys the sharing
1154  for(valuest::iterator v_it=values.begin();
1155  v_it!=values.end();
1156  v_it++)
1157  {
1158  object_mapt new_object_map;
1159 
1160  const object_map_dt &old_object_map=
1161  v_it->second.object_map.read();
1162 
1163  bool changed=false;
1164 
1165  forall_objects(o_it, old_object_map)
1166  {
1167  const exprt &object=object_numbering[o_it->first];
1168 
1169  if(object.id()==ID_dynamic_object)
1170  {
1172  to_dynamic_object_expr(object);
1173 
1174  if(to_mark.count(dynamic_object.get_instance())==0)
1175  set(new_object_map, *o_it);
1176  else
1177  {
1178  // adjust
1179  offsett o = o_it->second;
1180  exprt tmp(object);
1181  to_dynamic_object_expr(tmp).valid()=exprt(ID_unknown);
1182  insert(new_object_map, tmp, o);
1183  changed=true;
1184  }
1185  }
1186  else
1187  set(new_object_map, *o_it);
1188  }
1189 
1190  if(changed)
1191  v_it->second.object_map=new_object_map;
1192  }
1193 }
1194 
1196  const exprt &lhs,
1197  const object_mapt &values_rhs,
1198  const std::string &suffix,
1199  const namespacet &ns,
1200  assign_recursion_sett &recursion_set)
1201 {
1202  #if 0
1203  std::cout << "ASSIGN_REC LHS: " << format(lhs) << '\n';
1204  std::cout << "ASSIGN_REC SUFFIX: " << suffix << '\n';
1205 
1206  for(object_map_dt::const_iterator it=values_rhs.read().begin();
1207  it!=values_rhs.read().end(); it++)
1208  std::cout << "ASSIGN_REC RHS: " << to_expr(it) << '\n';
1209  #endif
1210 
1211  if(lhs.type().id()=="#REF#")
1212  {
1213  const irep_idt &ident = lhs.get(ID_identifier);
1214  object_mapt temp;
1215  gvs_recursion_sett recset;
1216  get_value_set_rec(lhs, temp, "", lhs.type().subtype(), ns, recset);
1217 
1218  if(recursion_set.find(ident)!=recursion_set.end())
1219  {
1220  recursion_set.insert(ident);
1221 
1222  forall_objects(it, temp.read())
1223  if(object_numbering[it->first].id()!=ID_unknown)
1224  assign_rec(object_numbering[it->first], values_rhs,
1225  suffix, ns, recursion_set);
1226 
1227  recursion_set.erase(ident);
1228  }
1229  }
1230  else if(lhs.id()==ID_symbol)
1231  {
1232  const irep_idt &identifier = to_symbol_expr(lhs).get_identifier();
1233 
1234  if(has_prefix(id2string(identifier),
1235  "value_set::dynamic_object") ||
1236  has_prefix(id2string(identifier),
1237  "value_set::return_value") ||
1238  values.find(id2string(identifier)+suffix)!=values.end())
1239  // otherwise we don't track this value
1240  {
1241  entryt &entry = get_entry(identifier, suffix);
1242 
1243  if(make_union(entry.object_map, values_rhs))
1244  changed = true;
1245  }
1246  }
1247  else if(lhs.id()==ID_dynamic_object)
1248  {
1251 
1252  const std::string name=
1253  "value_set::dynamic_object"+
1254  std::to_string(dynamic_object.get_instance());
1255 
1256  if(make_union(get_entry(name, suffix).object_map, values_rhs))
1257  changed = true;
1258  }
1259  else if(lhs.id()==ID_dereference)
1260  {
1261  if(lhs.operands().size()!=1)
1262  throw lhs.id_string()+" expected to have one operand";
1263 
1264  object_mapt reference_set;
1265  get_reference_set_sharing(lhs, reference_set, ns);
1266 
1267  forall_objects(it, reference_set.read())
1268  {
1269  const exprt &object=object_numbering[it->first];
1270 
1271  if(object.id()!=ID_unknown)
1272  assign_rec(object, values_rhs, suffix, ns, recursion_set);
1273  }
1274  }
1275  else if(lhs.id()==ID_index)
1276  {
1277  if(lhs.operands().size()!=2)
1278  throw "index expected to have two operands";
1279 
1280  const typet &type=ns.follow(lhs.op0().type());
1281 
1282  DATA_INVARIANT(type.id()==ID_array ||
1283  type.id()==ID_incomplete_array ||
1284  type.id()=="#REF#",
1285  "operand 0 of index expression must be an array");
1286 
1287  assign_rec(lhs.op0(), values_rhs, "[]"+suffix, ns, recursion_set);
1288  }
1289  else if(lhs.id()==ID_member)
1290  {
1291  if(lhs.operands().size()!=1)
1292  throw "member expected to have one operand";
1293 
1294  if(lhs.op0().is_nil())
1295  return;
1296 
1297  const std::string &component_name=lhs.get_string(ID_component_name);
1298 
1299  const typet &type=ns.follow(lhs.op0().type());
1300 
1301  DATA_INVARIANT(type.id()==ID_struct ||
1302  type.id()==ID_union ||
1303  type.id()==ID_incomplete_struct ||
1304  type.id()==ID_incomplete_union,
1305  "operand 0 of member expression must be struct or union");
1306 
1307  assign_rec(lhs.op0(), values_rhs, "."+component_name+suffix,
1308  ns, recursion_set);
1309  }
1310  else if(lhs.id()=="valid_object" ||
1311  lhs.id()=="dynamic_size" ||
1312  lhs.id()=="dynamic_type")
1313  {
1314  // we ignore this here
1315  }
1316  else if(lhs.id()==ID_string_constant)
1317  {
1318  // someone writes into a string-constant
1319  // evil guy
1320  }
1321  else if(lhs.id() == ID_null_object)
1322  {
1323  // evil as well
1324  }
1325  else if(lhs.id()==ID_typecast)
1326  {
1327  const typecast_exprt &typecast_expr=to_typecast_expr(lhs);
1328 
1329  assign_rec(typecast_expr.op(), values_rhs, suffix, ns, recursion_set);
1330  }
1331  else if(lhs.id()=="zero_string" ||
1332  lhs.id()=="is_zero_string" ||
1333  lhs.id()=="zero_string_length")
1334  {
1335  // ignore
1336  }
1337  else if(lhs.id()==ID_byte_extract_little_endian ||
1338  lhs.id()==ID_byte_extract_big_endian)
1339  {
1340  assert(lhs.operands().size()==2);
1341  assign_rec(lhs.op0(), values_rhs, suffix, ns, recursion_set);
1342  }
1343  else
1344  throw "assign NYI: `"+lhs.id_string()+"'";
1345 }
1346 
1348  const irep_idt &function,
1349  const exprt::operandst &arguments,
1350  const namespacet &ns)
1351 {
1352  const symbolt &symbol=ns.lookup(function);
1353 
1354  const code_typet &type=to_code_type(symbol.type);
1355  const code_typet::parameterst &parameter_types=type.parameters();
1356 
1357  // these first need to be assigned to dummy, temporary arguments
1358  // and only thereafter to the actuals, in order
1359  // to avoid overwriting actuals that are needed for recursive
1360  // calls
1361 
1362  for(std::size_t i=0; i<arguments.size(); i++)
1363  {
1364  const std::string identifier="value_set::" + id2string(function) + "::" +
1365  "argument$"+std::to_string(i);
1366  add_var(identifier, "");
1367  const symbol_exprt dummy_lhs(identifier, arguments[i].type());
1368  assign(dummy_lhs, arguments[i], ns);
1369  }
1370 
1371  // now assign to 'actual actuals'
1372 
1373  std::size_t i=0;
1374 
1375  for(code_typet::parameterst::const_iterator
1376  it=parameter_types.begin();
1377  it!=parameter_types.end();
1378  it++)
1379  {
1380  const irep_idt &identifier=it->get_identifier();
1381  if(identifier.empty())
1382  continue;
1383 
1384  add_var(identifier, "");
1385 
1386  const exprt v_expr=
1387  symbol_exprt("value_set::" + id2string(function) + "::" +
1388  "argument$"+std::to_string(i), it->type());
1389 
1390  const symbol_exprt actual_lhs(identifier, it->type());
1391  assign(actual_lhs, v_expr, ns);
1392  i++;
1393  }
1394 }
1395 
1397  const exprt &lhs,
1398  const namespacet &ns)
1399 {
1400  if(lhs.is_nil())
1401  return;
1402 
1403  std::string rvs = "value_set::return_value" + std::to_string(from_function);
1404  symbol_exprt rhs(rvs, lhs.type());
1405 
1406  assign(lhs, rhs, ns);
1407 }
1408 
1410  const exprt &code,
1411  const namespacet &ns)
1412 {
1413  const irep_idt &statement=code.get(ID_statement);
1414 
1415  if(statement==ID_block)
1416  {
1417  forall_operands(it, code)
1418  apply_code(*it, ns);
1419  }
1420  else if(statement==ID_function_call)
1421  {
1422  // shouldn't be here
1423  UNREACHABLE;
1424  }
1425  else if(statement==ID_assign ||
1426  statement==ID_init)
1427  {
1428  if(code.operands().size()!=2)
1429  throw "assignment expected to have two operands";
1430 
1431  assign(code.op0(), code.op1(), ns);
1432  }
1433  else if(statement==ID_decl)
1434  {
1435  if(code.operands().size()!=1)
1436  throw "decl expected to have one operand";
1437 
1438  const exprt &lhs=code.op0();
1439 
1440  if(lhs.id()!=ID_symbol)
1441  throw "decl expected to have symbol on lhs";
1442 
1443  assign(lhs, exprt(ID_invalid, lhs.type()), ns);
1444  }
1445  else if(statement==ID_expression)
1446  {
1447  // can be ignored, we don't expect side effects here
1448  }
1449  else if(statement==ID_cpp_delete ||
1450  statement==ID_cpp_delete_array)
1451  {
1452  // does nothing
1453  }
1454  else if(statement==ID_free)
1455  {
1456  // this may kill a valid bit
1457 
1458  if(code.operands().size()!=1)
1459  throw "free expected to have one operand";
1460 
1461  do_free(code.op0(), ns);
1462  }
1463  else if(statement=="lock" || statement=="unlock")
1464  {
1465  // ignore for now
1466  }
1467  else if(statement==ID_asm)
1468  {
1469  // ignore for now, probably not safe
1470  }
1471  else if(statement==ID_nondet)
1472  {
1473  // doesn't do anything
1474  }
1475  else if(statement==ID_printf)
1476  {
1477  // doesn't do anything
1478  }
1479  else if(statement==ID_return)
1480  {
1481  // this is turned into an assignment
1482  if(code.operands().size()==1)
1483  {
1484  std::string rvs="value_set::return_value"+std::to_string(from_function);
1485  symbol_exprt lhs(rvs, code.op0().type());
1486  assign(lhs, code.op0(), ns);
1487  }
1488  }
1489  else if(statement==ID_fence)
1490  {
1491  }
1492  else if(statement==ID_array_copy ||
1493  statement==ID_array_replace ||
1494  statement==ID_array_set)
1495  {
1496  }
1497  else if(statement==ID_input || statement==ID_output)
1498  {
1499  // doesn't do anything
1500  }
1501  else
1502  throw
1503  code.pretty()+"\n"+
1504  "value_set_fit: unexpected statement: "+id2string(statement);
1505 }
The type of an expression.
Definition: type.h:22
irep_idt name
The unique identifier.
Definition: symbol.h:43
void output(const namespacet &ns, std::ostream &out) const
data_typet::value_type value_type
Definition: value_set_fi.h:75
semantic type conversion
Definition: std_expr.h:2111
std::unordered_set< unsigned int > dynamic_object_id_sett
Definition: value_set_fi.h:190
BigInt mp_integer
Definition: mp_arith.h:22
Base type of functions.
Definition: std_types.h:764
bool is_nil() const
Definition: irep.h:172
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
bool is_not_nil() const
Definition: irep.h:173
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:106
std::unordered_set< idt, string_hash > flatten_seent
Definition: value_set_fi.h:200
std::unordered_set< exprt, irep_hash > expr_sett
Definition: value_set_fi.h:188
exprt & op0()
Definition: expr.h:72
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:641
const dynamic_object_exprt & to_dynamic_object_expr(const exprt &expr)
Cast a generic exprt to a dynamic_object_exprt.
Definition: std_expr.h:2076
const exprt & op() const
Definition: std_expr.h:340
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Definition: base_type.cpp:326
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
Definition: std_types.h:993
void do_free(const exprt &op, const namespacet &ns)
std::unordered_map< idt, entryt, string_hash > valuest
Definition: value_set_fi.h:199
void copy_to_operands(const exprt &expr)
Definition: expr.cpp:55
const irep_idt & get_identifier() const
Definition: std_expr.h:128
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
std::vector< parametert > parameterst
Definition: std_types.h:767
const componentst & components() const
Definition: std_types.h:245
static const char * alloc_adapter_prefix
bool is_true() const
Definition: expr.cpp:124
exprt to_expr(const object_map_dt::value_type &it) const
Value Set (Flow Insensitive, Sharing)
typet & type()
Definition: expr.h:56
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
static const object_map_dt blank
Definition: value_set_fi.h:98
void get_reference_set_sharing_rec(const exprt &expr, object_mapt &dest, const namespacet &ns) const
bool insert(object_mapt &dest, const object_map_dt::value_type &it) const
Definition: value_set_fi.h:113
void get_value_set_rec(const exprt &expr, object_mapt &dest, const std::string &suffix, const typet &original_type, const namespacet &ns, gvs_recursion_sett &recursion_set) const
void apply_code(const exprt &code, const namespacet &ns)
Extract member of struct or union.
Definition: std_expr.h:3869
std::unordered_set< idt, string_hash > gvs_recursion_sett
Definition: value_set_fi.h:201
unsigned from_function
Definition: value_set_fi.h:37
const irep_idt & id() const
Definition: irep.h:259
bool make_union(object_mapt &dest, const object_mapt &src) const
void flatten_rec(const entryt &, object_mapt &, flatten_seent &) const
The boolean constant true.
Definition: std_expr.h:4486
void get_reference_set(const exprt &expr, expr_sett &expr_set, const namespacet &ns) const
#define Forall_objects(it, map)
static object_numberingt object_numbering
Definition: value_set_fi.h:39
API to expression classes.
void assign_rec(const exprt &lhs, const object_mapt &values_rhs, const std::string &suffix, const namespacet &ns, assign_recursion_sett &recursion_set)
exprt & op1()
Definition: expr.h:75
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
TO_BE_DOCUMENTED.
Definition: namespace.h:74
entryt & get_entry(const idt &id, const std::string &suffix)
Definition: value_set_fi.h:235
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
split an expression into a base object and a (byte) offset
Definition: std_expr.h:1945
void do_function_call(const irep_idt &function, const exprt::operandst &arguments, const namespacet &ns)
#define forall_operands(it, expr)
Definition: expr.h:17
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
bitvector_typet index_type()
Definition: c_types.cpp:16
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
Author: Diffblue Ltd.
void get_value_set(const exprt &expr, std::list< exprt > &dest, const namespacet &ns) const
Operator to return the address of an object.
Definition: std_expr.h:3168
std::string from_type(const namespacet &ns, const irep_idt &identifier, const typet &type)
void flatten(const entryt &e, object_mapt &dest) const
bool is_constant() const
Definition: expr.cpp:119
valuest values
Definition: value_set_fi.h:263
std::vector< exprt > operandst
Definition: expr.h:45
const irep_idt & display_name() const
Definition: symbol.h:57
void do_end_function(const exprt &lhs, const namespacet &ns)
typet type
Type of symbol.
Definition: symbol.h:34
Base type of C structs and unions, and C++ classes.
Definition: std_types.h:162
std::unordered_set< idt, string_hash > assign_recursion_sett
Definition: value_set_fi.h:203
void get_reference_set_sharing(const exprt &expr, expr_sett &expr_set, const namespacet &ns) const
data_typet::const_iterator const_iterator
Definition: value_set_fi.h:73
Base class for all expressions.
Definition: expr.h:42
const parameterst & parameters() const
Definition: std_types.h:905
data_typet::iterator iterator
Definition: value_set_fi.h:71
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a generic typet to a struct_union_typet.
Definition: std_types.h:280
std::string to_string(const string_constraintt &expr)
Used for debug printing.
void dereference_rec(const exprt &src, exprt &dest) const
static hash_numbering< irep_idt, irep_id_hash > function_numbering
Definition: value_set_fi.h:40
bool offset_is_zero(const offsett &offset) const
Definition: value_set_fi.h:59
#define UNREACHABLE
Definition: invariant.h:271
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
Definition: std_expr.h:2143
const std::string & get_string(const irep_namet &name) const
Definition: irep.h:272
const T & read() const
const std::string & id_string() const
Definition: irep.h:262
void assign(const exprt &lhs, const exprt &rhs, const namespacet &ns)
bool is_zero() const
Definition: expr.cpp:161
void add_var(const idt &id, const std::string &suffix)
Definition: value_set_fi.h:225
Expression to hold a symbol (variable)
Definition: std_expr.h:90
exprt & op2()
Definition: expr.h:78
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:17
exprt dynamic_object(const exprt &pointer)
object_mapt object_map
Definition: value_set_fi.h:173
Base Type Computation.
const typet & subtype() const
Definition: type.h:33
#define DATA_INVARIANT(CONDITION, REASON)
Definition: invariant.h:278
TO_BE_DOCUMENTED.
Definition: std_expr.h:2035
operandst & operands()
Definition: expr.h:66
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
bool empty() const
Definition: dstring.h:73
void make_typecast(const typet &_type)
Definition: expr.cpp:84
const irept & find(const irep_namet &name) const
Definition: irep.cpp:285
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
Definition: namespace.cpp:136
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:286
unsigned from_target_index
Definition: value_set_fi.h:38
#define forall_objects(it, map)
optionalt< mp_integer > offsett
Represents the offset into an object: either a unique integer offset, or an unknown value...
Definition: value_set_fi.h:58
bool simplify(exprt &expr, const namespacet &ns)
array index operator
Definition: std_expr.h:1462
static format_containert< T > format(const T &o)
Definition: format.h:35