cprover
goto_rw.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening
6 
7 Date: April 2010
8 
9 \*******************************************************************/
10 
11 #include "goto_rw.h"
12 
13 #include <algorithm>
14 #include <limits>
15 #include <memory>
16 
17 #include <util/expr_util.h>
18 #include <util/std_code.h>
19 #include <util/std_expr.h>
21 #include <util/byte_operators.h>
22 #include <util/endianness_map.h>
23 #include <util/arith_tools.h>
24 #include <util/simplify_expr.h>
25 #include <util/make_unique.h>
26 
27 #include <langapi/language_util.h>
28 
30 
32 
34 {
35 }
36 
37 void range_domaint::output(const namespacet &, std::ostream &out) const
38 {
39  out << "[";
40  for(const_iterator itr=begin();
41  itr!=end();
42  ++itr)
43  {
44  if(itr!=begin())
45  out << ";";
46  out << itr->first << ":" << itr->second;
47  }
48  out << "]";
49 }
50 
52 {
53  for(rw_range_sett::objectst::iterator it=r_range_set.begin();
54  it!=r_range_set.end();
55  ++it)
56  it->second=nullptr;
57 
58  for(rw_range_sett::objectst::iterator it=w_range_set.begin();
59  it!=w_range_set.end();
60  ++it)
61  it->second=nullptr;
62 }
63 
64 void rw_range_sett::output(std::ostream &out) const
65 {
66  out << "READ:\n";
68  {
69  out << " " << it->first;
70  it->second->output(ns, out);
71  out << '\n';
72  }
73 
74  out << '\n';
75 
76  out << "WRITE:\n";
78  {
79  out << " " << it->first;
80  it->second->output(ns, out);
81  out << '\n';
82  }
83 }
84 
86  get_modet mode,
87  const exprt &expr,
88  const range_spect &range_start,
89  const range_spect &size)
90 {
91  const exprt &op=expr.op0();
92  assert(op.type().id()==ID_complex);
93 
94  range_spect sub_size=
96  assert(sub_size>0);
97  range_spect offset=
98  (range_start==-1 || expr.id()==ID_complex_real) ? 0 : sub_size;
99 
100  get_objects_rec(mode, op, range_start+offset, size);
101 }
102 
104  get_modet mode,
105  const if_exprt &if_expr,
106  const range_spect &range_start,
107  const range_spect &size)
108 {
109  if(if_expr.cond().is_false())
110  get_objects_rec(mode, if_expr.false_case(), range_start, size);
111  else if(if_expr.cond().is_true())
112  get_objects_rec(mode, if_expr.true_case(), range_start, size);
113  else
114  {
116 
117  get_objects_rec(mode, if_expr.false_case(), range_start, size);
118  get_objects_rec(mode, if_expr.true_case(), range_start, size);
119  }
120 }
121 
123  get_modet mode,
124  const dereference_exprt &deref,
125  const range_spect &,
126  const range_spect &)
127 {
128  const exprt &pointer=deref.pointer();
130  if(mode!=get_modet::READ)
131  get_objects_rec(mode, pointer);
132 }
133 
135  get_modet mode,
136  const byte_extract_exprt &be,
137  const range_spect &range_start,
138  const range_spect &size)
139 {
140  const exprt simp_offset=simplify_expr(be.offset(), ns);
141 
142  mp_integer index;
143  if(range_start==-1 || to_integer(simp_offset, index))
144  get_objects_rec(mode, be.op(), -1, size);
145  else
146  {
147  index*=8;
148  if(index>=pointer_offset_bits(be.op().type(), ns))
149  return;
150 
151  endianness_mapt map(
152  be.op().type(),
153  be.id()==ID_byte_extract_little_endian,
154  ns);
155  assert(index<std::numeric_limits<size_t>::max());
156  range_spect offset=range_start + map.map_bit(integer2size_t(index));
157  get_objects_rec(mode, be.op(), offset, size);
158  }
159 }
160 
162  get_modet mode,
163  const shift_exprt &shift,
164  const range_spect &range_start,
165  const range_spect &size)
166 {
167  const exprt simp_distance=simplify_expr(shift.distance(), ns);
168 
169  range_spect src_size=
171 
172  mp_integer dist;
173  if(range_start==-1 ||
174  size==-1 ||
175  src_size==-1 ||
176  to_integer(simp_distance, dist))
177  {
178  get_objects_rec(mode, shift.op(), -1, -1);
179  get_objects_rec(mode, shift.distance(), -1, -1);
180  }
181  else
182  {
183  range_spect dist_r=to_range_spect(dist);
184 
185  // not sure whether to worry about
186  // config.ansi_c.endianness==configt::ansi_ct::IS_LITTLE_ENDIAN
187  // right here maybe?
188 
189  if(shift.id()==ID_ashr || shift.id()==ID_lshr)
190  {
191  range_spect sh_range_start=range_start;
192  sh_range_start+=dist_r;
193 
194  range_spect sh_size=std::min(size, src_size-sh_range_start);
195 
196  if(sh_range_start>=0 && sh_range_start<src_size)
197  get_objects_rec(mode, shift.op(), sh_range_start, sh_size);
198  }
199  else
200  {
201  assert(src_size-dist_r>=0);
202  range_spect sh_size=std::min(size, src_size-dist_r);
203 
204  get_objects_rec(mode, shift.op(), range_start, sh_size);
205  }
206  }
207 }
208 
210  get_modet mode,
211  const member_exprt &expr,
212  const range_spect &range_start,
213  const range_spect &size)
214 {
215  const typet &type=ns.follow(expr.struct_op().type());
216 
217  if(type.id()==ID_union ||
218  range_start==-1)
219  {
220  get_objects_rec(mode, expr.struct_op(), range_start, size);
221  return;
222  }
223 
224  const struct_typet &struct_type=to_struct_type(type);
225 
226  range_spect offset=
229  struct_type,
230  expr.get_component_name(),
231  ns));
232 
233  if(offset!=-1)
234  offset+=range_start;
235 
236  get_objects_rec(mode, expr.struct_op(), offset, size);
237 }
238 
240  get_modet mode,
241  const index_exprt &expr,
242  const range_spect &range_start,
243  const range_spect &size)
244 {
245  if(expr.array().id() == ID_null_object)
246  return;
247 
248  range_spect sub_size=0;
249  const typet &type=ns.follow(expr.array().type());
250 
251  if(type.id()==ID_vector)
252  {
253  const vector_typet &vector_type=to_vector_type(type);
254 
255  sub_size=
256  to_range_spect(pointer_offset_bits(vector_type.subtype(), ns));
257  }
258  else if(type.id()==ID_array)
259  {
260  const array_typet &array_type=to_array_type(type);
261 
262  sub_size=
264  }
265  else
266  return;
267 
268  const exprt simp_index=simplify_expr(expr.index(), ns);
269 
270  mp_integer index;
271  if(to_integer(simp_index, index))
272  {
274  index=-1;
275  }
276 
277  if(range_start==-1 ||
278  sub_size==-1 ||
279  index==-1)
280  get_objects_rec(mode, expr.array(), -1, size);
281  else
283  mode,
284  expr.array(),
285  range_start+to_range_spect(index*sub_size),
286  size);
287 }
288 
290  get_modet mode,
291  const array_exprt &expr,
292  const range_spect &range_start,
293  const range_spect &size)
294 {
295  const array_typet &array_type=
296  to_array_type(ns.follow(expr.type()));
297 
298  range_spect sub_size=
300 
301  if(sub_size==-1)
302  {
303  forall_operands(it, expr)
304  get_objects_rec(mode, *it, 0, -1);
305 
306  return;
307  }
308 
309  range_spect offset=0;
310  range_spect full_r_s=range_start==-1 ? 0 : range_start;
311  range_spect full_r_e=
312  size==-1 ? sub_size*expr.operands().size() : full_r_s+size;
313 
314  forall_operands(it, expr)
315  {
316  if(full_r_s<=offset+sub_size && full_r_e>offset)
317  {
318  range_spect cur_r_s=full_r_s<=offset ? 0 : full_r_s-offset;
319  range_spect cur_r_e=
320  full_r_e>offset+sub_size ? sub_size : full_r_e-offset;
321 
322  get_objects_rec(mode, *it, cur_r_s, cur_r_e-cur_r_s);
323  }
324 
325  offset+=sub_size;
326  }
327 }
328 
330  get_modet mode,
331  const struct_exprt &expr,
332  const range_spect &range_start,
333  const range_spect &size)
334 {
335  const struct_typet &struct_type=
336  to_struct_type(ns.follow(expr.type()));
337 
338  range_spect full_size=
339  to_range_spect(pointer_offset_bits(struct_type, ns));
340 
341  range_spect offset=0;
342  range_spect full_r_s=range_start==-1 ? 0 : range_start;
343  range_spect full_r_e=size==-1 || full_size==-1 ? -1 : full_r_s+size;
344 
345  forall_operands(it, expr)
346  {
347  range_spect sub_size=
348  to_range_spect(pointer_offset_bits(it->type(), ns));
349 
350  if(offset==-1)
351  {
352  get_objects_rec(mode, *it, 0, sub_size);
353  }
354  else if(sub_size==-1)
355  {
356  if(full_r_e==-1 || full_r_e>offset)
357  {
358  range_spect cur_r_s=full_r_s<=offset ? 0 : full_r_s-offset;
359 
360  get_objects_rec(mode, *it, cur_r_s, -1);
361  }
362 
363  offset=-1;
364  }
365  else if(full_r_e==-1)
366  {
367  if(full_r_s<=offset+sub_size)
368  {
369  range_spect cur_r_s=full_r_s<=offset ? 0 : full_r_s-offset;
370 
371  get_objects_rec(mode, *it, cur_r_s, sub_size-cur_r_s);
372  }
373 
374  offset+=sub_size;
375  }
376  else if(full_r_s<=offset+sub_size && full_r_e>offset)
377  {
378  range_spect cur_r_s=full_r_s<=offset ? 0 : full_r_s-offset;
379  range_spect cur_r_e=
380  full_r_e>offset+sub_size ? sub_size : full_r_e-offset;
381 
382  get_objects_rec(mode, *it, cur_r_s, cur_r_e-cur_r_s);
383 
384  offset+=sub_size;
385  }
386  }
387 }
388 
390  get_modet mode,
391  const typecast_exprt &tc,
392  const range_spect &range_start,
393  const range_spect &size)
394 {
395  const exprt &op=tc.op();
396 
397  range_spect new_size=
399 
400  if(range_start==-1)
401  new_size=-1;
402  else if(new_size!=-1)
403  {
404  if(new_size<=range_start)
405  return;
406 
407  new_size-=range_start;
408  new_size=std::min(size, new_size);
409  }
410 
411  get_objects_rec(mode, op, range_start, new_size);
412 }
413 
415 {
416  if(object.id() == ID_string_constant ||
417  object.id() == ID_label ||
418  object.id() == ID_array ||
419  object.id() == ID_null_object)
420  // constant, nothing to do
421  return;
422  else if(object.id()==ID_symbol)
424  else if(object.id()==ID_dereference)
426  else if(object.id()==ID_index)
427  {
428  const index_exprt &index=to_index_expr(object);
429 
432  }
433  else if(object.id()==ID_member)
434  {
435  const member_exprt &member=to_member_expr(object);
436 
438  }
439  else if(object.id()==ID_if)
440  {
441  const if_exprt &if_expr=to_if_expr(object);
442 
446  }
447  else if(object.id()==ID_byte_extract_little_endian ||
448  object.id()==ID_byte_extract_big_endian)
449  {
450  const byte_extract_exprt &be=to_byte_extract_expr(object);
451 
453  }
454  else if(object.id()==ID_typecast)
455  {
456  const typecast_exprt &tc=to_typecast_expr(object);
457 
459  }
460  else
461  throw "rw_range_sett: address_of `"+object.id_string()+"' not handled";
462 }
463 
465  get_modet mode,
466  const irep_idt &identifier,
467  const range_spect &range_start,
468  const range_spect &range_end)
469 {
470  objectst::iterator entry=
472  .insert(
473  std::pair<const irep_idt &, std::unique_ptr<range_domain_baset>>(
474  identifier, nullptr))
475  .first;
476 
477  if(entry->second==nullptr)
478  entry->second=util_make_unique<range_domaint>();
479 
480  static_cast<range_domaint&>(*entry->second).push_back(
481  {range_start, range_end});
482 }
483 
485  get_modet mode,
486  const exprt &expr,
487  const range_spect &range_start,
488  const range_spect &size)
489 {
490  if(expr.id()==ID_complex_real ||
491  expr.id()==ID_complex_imag)
492  get_objects_complex(mode, expr, range_start, size);
493  else if(expr.id()==ID_typecast)
495  mode,
496  to_typecast_expr(expr),
497  range_start,
498  size);
499  else if(expr.id()==ID_if)
500  get_objects_if(mode, to_if_expr(expr), range_start, size);
501  else if(expr.id()==ID_dereference)
503  mode,
504  to_dereference_expr(expr),
505  range_start,
506  size);
507  else if(expr.id()==ID_byte_extract_little_endian ||
508  expr.id()==ID_byte_extract_big_endian)
510  mode,
511  to_byte_extract_expr(expr),
512  range_start,
513  size);
514  else if(expr.id()==ID_shl ||
515  expr.id()==ID_ashr ||
516  expr.id()==ID_lshr)
517  get_objects_shift(mode, to_shift_expr(expr), range_start, size);
518  else if(expr.id()==ID_member)
519  get_objects_member(mode, to_member_expr(expr), range_start, size);
520  else if(expr.id()==ID_index)
521  get_objects_index(mode, to_index_expr(expr), range_start, size);
522  else if(expr.id()==ID_array)
523  get_objects_array(mode, to_array_expr(expr), range_start, size);
524  else if(expr.id()==ID_struct)
525  get_objects_struct(mode, to_struct_expr(expr), range_start, size);
526  else if(expr.id()==ID_symbol)
527  {
528  const symbol_exprt &symbol=to_symbol_expr(expr);
529  const irep_idt identifier=symbol.get_identifier();
530  range_spect full_size=
532 
533  if(full_size==0 ||
534  (full_size>0 && range_start>=full_size))
535  {
536  // nothing to do, these are effectively constants (like function
537  // symbols or structs with no members)
538  // OR: invalid memory accesses
539  }
540  else if(range_start>=0)
541  {
542  range_spect range_end=size==-1 ? -1 : range_start+size;
543  if(size!=-1 && full_size!=-1)
544  range_end=std::min(range_end, full_size);
545 
546  add(mode, identifier, range_start, range_end);
547  }
548  else
549  add(mode, identifier, 0, -1);
550  }
551  else if(mode==get_modet::READ && expr.id()==ID_address_of)
553  else if(mode==get_modet::READ)
554  {
555  // possibly affects the full object size, even if range_start/size
556  // are only a subset of the bytes (e.g., when using the result of
557  // arithmetic operations)
558  forall_operands(it, expr)
559  get_objects_rec(mode, *it);
560  }
561  else if(expr.id() == ID_null_object ||
562  expr.id() == ID_string_constant)
563  {
564  // dereferencing may yield some weird ones, ignore these
565  }
566  else if(mode==get_modet::LHS_W)
567  {
568  forall_operands(it, expr)
569  get_objects_rec(mode, *it);
570  }
571  else
572  throw "rw_range_sett: assignment to `"+expr.id_string()+"' not handled";
573 }
574 
576 {
577  range_spect size=
579  get_objects_rec(mode, expr, 0, size);
580 }
581 
583 {
584  // TODO should recurse into various composite types
585  if(type.id()==ID_array)
586  {
587  get_objects_rec(type.subtype());
589  }
590 }
591 
593  get_modet mode,
594  const dereference_exprt &deref,
595  const range_spect &range_start,
596  const range_spect &size)
597 {
599  mode,
600  deref,
601  range_start,
602  size);
603 
604  exprt object=deref;
605  dereference(target, object, ns, value_sets);
606 
607  range_spect new_size=
608  to_range_spect(pointer_offset_bits(object.type(), ns));
609 
610  if(range_start==-1 || new_size<=range_start)
611  new_size=-1;
612  else
613  {
614  new_size-=range_start;
615  new_size=std::min(size, new_size);
616  }
617 
618  // value_set_dereferencet::build_reference_to will turn *p into
619  // DYNAMIC_OBJECT(p) ? *p : invalid_objectN
620  if(object.is_not_nil() && !has_subexpr(object, ID_dereference))
621  get_objects_rec(mode, object, range_start, new_size);
622 }
623 
625  const namespacet &ns, std::ostream &out) const
626 {
627  out << "[";
628  for(const_iterator itr=begin();
629  itr!=end();
630  ++itr)
631  {
632  if(itr!=begin())
633  out << ";";
634  out << itr->first << ":" << itr->second.first;
635  // we don't know what mode (language) we are in, so we rely on the default
636  // language to be reasonable for from_expr
637  out << " if " << from_expr(ns, "", itr->second.second);
638  }
639  out << "]";
640 }
641 
643  get_modet mode,
644  const if_exprt &if_expr,
645  const range_spect &range_start,
646  const range_spect &size)
647 {
648  if(if_expr.cond().is_false())
649  get_objects_rec(mode, if_expr.false_case(), range_start, size);
650  else if(if_expr.cond().is_true())
651  get_objects_rec(mode, if_expr.true_case(), range_start, size);
652  else
653  {
655 
656  guardt guard_bak1(guard), guard_bak2(guard);
657 
658  guard.add(not_exprt(if_expr.cond()));
659  get_objects_rec(mode, if_expr.false_case(), range_start, size);
660  guard.swap(guard_bak1);
661 
662  guard.add(if_expr.cond());
663  get_objects_rec(mode, if_expr.true_case(), range_start, size);
664  guard.swap(guard_bak2);
665  }
666 }
667 
669  get_modet mode,
670  const irep_idt &identifier,
671  const range_spect &range_start,
672  const range_spect &range_end)
673 {
674  objectst::iterator entry=
676  .insert(
677  std::pair<const irep_idt &, std::unique_ptr<range_domain_baset>>(
678  identifier, nullptr))
679  .first;
680 
681  if(entry->second==nullptr)
682  entry->second=util_make_unique<guarded_range_domaint>();
683 
684  static_cast<guarded_range_domaint&>(*entry->second).insert(
685  {range_start, {range_end, guard.as_expr()}});
686 }
687 
689  const code_assignt &assign,
690  rw_range_sett &rw_set)
691 {
692  rw_set.get_objects_rec(target, rw_range_sett::get_modet::LHS_W, assign.lhs());
693  rw_set.get_objects_rec(target, rw_range_sett::get_modet::READ, assign.rhs());
694 }
695 
697  const code_function_callt &function_call,
698  rw_range_sett &rw_set)
699 {
700  if(function_call.lhs().is_not_nil())
701  rw_set.get_objects_rec(
702  target,
704  function_call.lhs());
705 
706  rw_set.get_objects_rec(
707  target,
709  function_call.function());
710 
711  forall_expr(it, function_call.arguments())
712  rw_set.get_objects_rec(target, rw_range_sett::get_modet::READ, *it);
713 }
714 
716  rw_range_sett &rw_set)
717 {
718  switch(target->type)
719  {
720  case NO_INSTRUCTION_TYPE:
721  case INCOMPLETE_GOTO:
722  UNREACHABLE;
723  break;
724 
725  case GOTO:
726  case ASSUME:
727  case ASSERT:
728  rw_set.get_objects_rec(
729  target,
731  target->guard);
732  break;
733 
734  case RETURN:
735  {
736  const code_returnt &code_return=
737  to_code_return(target->code);
738  if(code_return.has_return_value())
739  rw_set.get_objects_rec(
740  target,
742  code_return.return_value());
743  }
744  break;
745 
746  case OTHER:
747  // if it's printf, mark the operands as read here
748  if(target->code.get(ID_statement)==ID_printf)
749  {
750  forall_expr(it, target->code.operands())
751  rw_set.get_objects_rec(target, rw_range_sett::get_modet::READ, *it);
752  }
753  break;
754 
755  case SKIP:
756  case START_THREAD:
757  case END_THREAD:
758  case LOCATION:
759  case END_FUNCTION:
760  case ATOMIC_BEGIN:
761  case ATOMIC_END:
762  case THROW:
763  case CATCH:
764  // these don't read or write anything
765  break;
766 
767  case ASSIGN:
768  goto_rw(target, to_code_assign(target->code), rw_set);
769  break;
770 
771  case DEAD:
772  rw_set.get_objects_rec(
773  target,
775  to_code_dead(target->code).symbol());
776  break;
777 
778  case DECL:
779  rw_set.get_objects_rec(
780  to_code_decl(target->code).symbol().type());
781  rw_set.get_objects_rec(
782  target,
784  to_code_decl(target->code).symbol());
785  break;
786 
787  case FUNCTION_CALL:
788  goto_rw(target, to_code_function_call(target->code), rw_set);
789  break;
790  }
791 }
792 
794 {
796  goto_rw(i_it, rw_set);
797 }
798 
799 void goto_rw(const goto_functionst &goto_functions,
800  const irep_idt &function,
801  rw_range_sett &rw_set)
802 {
803  goto_functionst::function_mapt::const_iterator f_it=
804  goto_functions.function_map.find(function);
805 
806  if(f_it!=goto_functions.function_map.end())
807  {
808  const goto_programt &body=f_it->second.body;
809 
810  goto_rw(body, rw_set);
811  }
812 }
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
Definition: std_expr.h:3424
The type of an expression.
Definition: type.h:22
exprt as_expr() const
Definition: guard.h:43
goto_programt::const_targett target
Definition: goto_rw.h:277
const exprt & return_value() const
Definition: std_code.h:937
Boolean negation.
Definition: std_expr.h:3228
const code_declt & to_code_decl(const codet &code)
Definition: std_code.h:291
exprt & true_case()
Definition: std_expr.h:3393
sub_typet::const_iterator const_iterator
Definition: goto_rw.h:84
semantic type conversion
Definition: std_expr.h:2111
BigInt mp_integer
Definition: mp_arith.h:22
bool is_not_nil() const
Definition: irep.h:173
Maps a big-endian offset to a little-endian offset.
exprt & object()
Definition: std_expr.h:3178
#define forall_rw_range_set_w_objects(it, rw_set)
Definition: goto_rw.h:28
iterator begin()
Definition: goto_rw.h:299
exprt & op0()
Definition: expr.h:72
exprt simplify_expr(const exprt &src, const namespacet &ns)
const code_deadt & to_code_dead(const codet &code)
Definition: std_code.h:344
value_setst & value_sets
Definition: goto_rw.h:275
const exprt & op() const
Definition: std_expr.h:340
sub_typet::const_iterator const_iterator
Definition: goto_rw.h:297
exprt & symbol()
Definition: std_code.h:268
const array_exprt & to_array_expr(const exprt &expr)
Cast a generic exprt to an array_exprt.
Definition: std_expr.h:1640
Deprecated expression utility functions.
const irep_idt & get_identifier() const
Definition: std_expr.h:128
#define forall_expr(it, expr)
Definition: expr.h:28
Goto Programs with Functions.
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
range_spect to_range_spect(const mp_integer &size)
Definition: goto_rw.h:63
bool is_false() const
Definition: expr.cpp:131
virtual ~rw_range_sett()
Definition: goto_rw.cpp:51
int range_spect
Definition: goto_rw.h:61
virtual void get_objects_dereference(get_modet mode, const dereference_exprt &deref, const range_spect &range_start, const range_spect &size)
Definition: goto_rw.cpp:592
virtual void get_objects_member(get_modet mode, const member_exprt &expr, const range_spect &range_start, const range_spect &size)
Definition: goto_rw.cpp:209
The trinary if-then-else operator.
Definition: std_expr.h:3359
exprt & cond()
Definition: std_expr.h:3383
bool is_true() const
Definition: expr.cpp:124
virtual void get_objects_index(get_modet mode, const index_exprt &expr, const range_spect &range_start, const range_spect &size)
Definition: goto_rw.cpp:239
Definition: guard.h:19
function_mapt function_map
virtual void get_objects_complex(get_modet mode, const exprt &expr, const range_spect &range_start, const range_spect &size)
Definition: goto_rw.cpp:85
mp_integer pointer_offset_bits(const typet &type, const namespacet &ns)
typet & type()
Definition: expr.h:56
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast a generic exprt to an address_of_exprt.
Definition: std_expr.h:3199
exprt & distance()
Definition: std_expr.h:2797
Structure type.
Definition: std_types.h:297
virtual void get_objects_struct(get_modet mode, const struct_exprt &expr, const range_spect &range_start, const range_spect &size)
Definition: goto_rw.cpp:329
objectst r_range_set
Definition: goto_rw.h:158
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast a generic exprt to a dereference_exprt.
Definition: std_expr.h:3326
iterator end()
Definition: goto_rw.h:90
Extract member of struct or union.
Definition: std_expr.h:3869
void output(const namespacet &ns, std::ostream &out) const override
Definition: goto_rw.cpp:37
virtual void get_objects_if(get_modet mode, const if_exprt &if_expr, const range_spect &range_start, const range_spect &size)
Definition: goto_rw.cpp:642
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:240
const irep_idt & id() const
Definition: irep.h:259
exprt & lhs()
Definition: std_code.h:209
objectst w_range_set
Definition: goto_rw.h:158
const namespacet & ns
Definition: goto_rw.h:156
Expression classes for byte-level operators.
argumentst & arguments()
Definition: std_code.h:890
exprt dereference(const exprt &pointer, const namespacet &ns)
Definition: dereference.h:88
virtual void get_objects_address_of(const exprt &object)
Definition: goto_rw.cpp:414
virtual void add(get_modet mode, const irep_idt &identifier, const range_spect &range_start, const range_spect &range_end)
Definition: goto_rw.cpp:464
bool has_subexpr(const exprt &expr, const std::function< bool(const exprt &)> &pred)
returns true if the expression has a subexpression that satisfies pred
Definition: expr_util.cpp:138
exprt & rhs()
Definition: std_code.h:214
Operator to dereference a pointer.
Definition: std_expr.h:3282
A constant-size array type.
Definition: std_types.h:1638
API to expression classes.
virtual void get_objects_byte_extract(get_modet mode, const byte_extract_exprt &be, const range_spect &range_start, const range_spect &size)
Definition: goto_rw.cpp:134
instructionst::const_iterator const_targett
Definition: goto_program.h:398
TO_BE_DOCUMENTED.
Definition: namespace.h:74
virtual void get_objects_if(get_modet mode, const if_exprt &if_expr, const range_spect &range_start, const range_spect &size)
Definition: goto_rw.cpp:103
void goto_rw(goto_programt::const_targett target, const code_assignt &assign, rw_range_sett &rw_set)
Definition: goto_rw.cpp:688
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
Definition: std_expr.h:3953
const code_returnt & to_code_return(const codet &code)
Definition: std_code.h:963
const vector_typet & to_vector_type(const typet &type)
Cast a generic typet to a vector_typet.
Definition: std_types.h:1669
virtual void get_objects_rec(goto_programt::const_targett, get_modet mode, const exprt &expr)
Definition: goto_rw.h:143
A function call.
Definition: std_code.h:858
#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
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
Definition: std_types.h:318
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
virtual void get_objects_shift(get_modet mode, const shift_exprt &shift, const range_spect &range_start, const range_spect &size)
Definition: goto_rw.cpp:161
Operator to return the address of an object.
Definition: std_expr.h:3168
const struct_exprt & to_struct_expr(const exprt &expr)
Cast a generic exprt to a struct_exprt.
Definition: std_expr.h:1838
exprt & symbol()
Definition: std_code.h:321
exprt & false_case()
Definition: std_expr.h:3403
virtual void add(get_modet mode, const irep_idt &identifier, const range_spect &range_start, const range_spect &range_end)
Definition: goto_rw.cpp:668
virtual void get_objects_array(get_modet mode, const array_exprt &expr, const range_spect &range_start, const range_spect &size)
Definition: goto_rw.cpp:289
bool has_return_value() const
Definition: std_code.h:947
Pointer Logic.
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:70
#define forall_rw_range_set_r_objects(it, rw_set)
Definition: goto_rw.h:24
virtual void get_objects_typecast(get_modet mode, const typecast_exprt &tc, const range_spect &range_start, const range_spect &size)
Definition: goto_rw.cpp:389
virtual void get_objects_dereference(get_modet mode, const dereference_exprt &deref, const range_spect &range_start, const range_spect &size)
Definition: goto_rw.cpp:122
iterator end()
Definition: goto_rw.h:303
const shift_exprt & to_shift_expr(const exprt &expr)
Cast a generic exprt to a shift_exprt.
Definition: std_expr.h:2818
exprt & index()
Definition: std_expr.h:1496
exprt & op()
Definition: std_expr.h:2787
exprt & function()
Definition: std_code.h:878
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Definition: std_types.h:1054
Base class for all expressions.
Definition: expr.h:42
exprt & pointer()
Definition: std_expr.h:3305
const exprt & struct_op() const
Definition: std_expr.h:3909
irep_idt get_component_name() const
Definition: std_expr.h:3893
#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
virtual void output(const namespacet &ns, std::ostream &out) const override
Definition: goto_rw.cpp:624
virtual void get_objects_rec(goto_programt::const_targett _target, get_modet mode, const exprt &expr)
Definition: goto_rw.h:335
const std::string & id_string() const
Definition: irep.h:262
void swap(irept &irep)
Definition: irep.h:303
goto_programt & goto_program
Definition: cover.cpp:63
arrays with given size
Definition: std_types.h:1013
Expression to hold a symbol (variable)
Definition: std_expr.h:90
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:17
virtual ~range_domain_baset()
Definition: goto_rw.cpp:33
virtual void get_objects_rec(goto_programt::const_targett _target, get_modet mode, const exprt &expr)
Definition: goto_rw.h:264
Return from a function.
Definition: std_code.h:923
std::size_t integer2size_t(const mp_integer &n)
Definition: mp_arith.cpp:195
const typet & subtype() const
Definition: type.h:33
operandst & operands()
Definition: expr.h:66
mp_integer member_offset_bits(const struct_typet &type, const irep_idt &member, const namespacet &ns)
TO_BE_DOCUMENTED.
struct constructor from list of elements
Definition: std_expr.h:1815
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:735
exprt & array()
Definition: std_expr.h:1486
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
Definition: std_expr.h:1517
A base class for shift operators.
Definition: std_expr.h:2765
void output(std::ostream &out) const
Definition: goto_rw.cpp:64
array constructor from list of elements
Definition: std_expr.h:1617
Assignment.
Definition: std_code.h:196
void add(const exprt &expr)
Definition: guard.cpp:64
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:909
iterator begin()
Definition: goto_rw.h:86
array index operator
Definition: std_expr.h:1462