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 
38  const namespacet &ns, std::ostream &out) const
39 {
40  out << "[";
41  for(const_iterator itr=begin();
42  itr!=end();
43  ++itr)
44  {
45  if(itr!=begin())
46  out << ";";
47  out << itr->first << ":" << itr->second;
48  }
49  out << "]";
50 }
51 
53 {
54  for(rw_range_sett::objectst::iterator it=r_range_set.begin();
55  it!=r_range_set.end();
56  ++it)
57  it->second=nullptr;
58 
59  for(rw_range_sett::objectst::iterator it=w_range_set.begin();
60  it!=w_range_set.end();
61  ++it)
62  it->second=nullptr;
63 }
64 
65 void rw_range_sett::output(std::ostream &out) const
66 {
67  out << "READ:\n";
69  {
70  out << " " << it->first;
71  it->second->output(ns, out);
72  out << '\n';
73  }
74 
75  out << '\n';
76 
77  out << "WRITE:\n";
79  {
80  out << " " << it->first;
81  it->second->output(ns, out);
82  out << '\n';
83  }
84 }
85 
87  get_modet mode,
88  const exprt &expr,
89  const range_spect &range_start,
90  const range_spect &size)
91 {
92  const exprt &op=expr.op0();
93  assert(op.type().id()==ID_complex);
94 
95  range_spect sub_size=
97  assert(sub_size>0);
98  range_spect offset=
99  (range_start==-1 || expr.id()==ID_complex_real) ? 0 : sub_size;
100 
101  get_objects_rec(mode, op, range_start+offset, size);
102 }
103 
105  get_modet mode,
106  const if_exprt &if_expr,
107  const range_spect &range_start,
108  const range_spect &size)
109 {
110  if(if_expr.cond().is_false())
111  get_objects_rec(mode, if_expr.false_case(), range_start, size);
112  else if(if_expr.cond().is_true())
113  get_objects_rec(mode, if_expr.true_case(), range_start, size);
114  else
115  {
117 
118  get_objects_rec(mode, if_expr.false_case(), range_start, size);
119  get_objects_rec(mode, if_expr.true_case(), range_start, size);
120  }
121 }
122 
124  get_modet mode,
125  const dereference_exprt &deref,
126  const range_spect &range_start,
127  const range_spect &size)
128 {
129  const exprt &pointer=deref.pointer();
131  if(mode!=get_modet::READ)
132  get_objects_rec(mode, pointer);
133 }
134 
136  get_modet mode,
137  const byte_extract_exprt &be,
138  const range_spect &range_start,
139  const range_spect &size)
140 {
141  const exprt simp_offset=simplify_expr(be.offset(), ns);
142 
143  mp_integer index;
144  if(range_start==-1 || to_integer(simp_offset, index))
145  get_objects_rec(mode, be.op(), -1, size);
146  else
147  {
148  index*=8;
149  if(index>=pointer_offset_bits(be.op().type(), ns))
150  return;
151 
152  endianness_mapt map(
153  be.op().type(),
154  be.id()==ID_byte_extract_little_endian,
155  ns);
156  assert(index<std::numeric_limits<size_t>::max());
157  range_spect offset=range_start + map.map_bit(integer2size_t(index));
158  get_objects_rec(mode, be.op(), offset, size);
159  }
160 }
161 
163  get_modet mode,
164  const shift_exprt &shift,
165  const range_spect &range_start,
166  const range_spect &size)
167 {
168  const exprt simp_distance=simplify_expr(shift.distance(), ns);
169 
170  range_spect src_size=
172 
173  mp_integer dist;
174  if(range_start==-1 ||
175  size==-1 ||
176  src_size==-1 ||
177  to_integer(simp_distance, dist))
178  {
179  get_objects_rec(mode, shift.op(), -1, -1);
180  get_objects_rec(mode, shift.distance(), -1, -1);
181  }
182  else
183  {
184  range_spect dist_r=to_range_spect(dist);
185 
186  // not sure whether to worry about
187  // config.ansi_c.endianness==configt::ansi_ct::IS_LITTLE_ENDIAN
188  // right here maybe?
189 
190  if(shift.id()==ID_ashr || shift.id()==ID_lshr)
191  {
192  range_spect sh_range_start=range_start;
193  sh_range_start+=dist_r;
194 
195  range_spect sh_size=std::min(size, src_size-sh_range_start);
196 
197  if(sh_range_start>=0 && sh_range_start<src_size)
198  get_objects_rec(mode, shift.op(), sh_range_start, sh_size);
199  }
200  else
201  {
202  assert(src_size-dist_r>=0);
203  range_spect sh_size=std::min(size, src_size-dist_r);
204 
205  get_objects_rec(mode, shift.op(), range_start, sh_size);
206  }
207  }
208 }
209 
211  get_modet mode,
212  const member_exprt &expr,
213  const range_spect &range_start,
214  const range_spect &size)
215 {
216  const typet &type=ns.follow(expr.struct_op().type());
217 
218  if(type.id()==ID_union ||
219  range_start==-1)
220  {
221  get_objects_rec(mode, expr.struct_op(), range_start, size);
222  return;
223  }
224 
225  const struct_typet &struct_type=to_struct_type(type);
226 
227  range_spect offset=
230  struct_type,
231  expr.get_component_name(),
232  ns));
233 
234  if(offset!=-1)
235  offset+=range_start;
236 
237  get_objects_rec(mode, expr.struct_op(), offset, size);
238 }
239 
241  get_modet mode,
242  const index_exprt &expr,
243  const range_spect &range_start,
244  const range_spect &size)
245 {
246  if(expr.array().id() == ID_null_object)
247  return;
248 
249  range_spect sub_size=0;
250  const typet &type=ns.follow(expr.array().type());
251 
252  if(type.id()==ID_vector)
253  {
254  const vector_typet &vector_type=to_vector_type(type);
255 
256  sub_size=
257  to_range_spect(pointer_offset_bits(vector_type.subtype(), ns));
258  }
259  else if(type.id()==ID_array)
260  {
261  const array_typet &array_type=to_array_type(type);
262 
263  sub_size=
265  }
266  else
267  return;
268 
269  const exprt simp_index=simplify_expr(expr.index(), ns);
270 
271  mp_integer index;
272  if(to_integer(simp_index, index))
273  {
275  index=-1;
276  }
277 
278  if(range_start==-1 ||
279  sub_size==-1 ||
280  index==-1)
281  get_objects_rec(mode, expr.array(), -1, size);
282  else
284  mode,
285  expr.array(),
286  range_start+to_range_spect(index*sub_size),
287  size);
288 }
289 
291  get_modet mode,
292  const array_exprt &expr,
293  const range_spect &range_start,
294  const range_spect &size)
295 {
296  const array_typet &array_type=
297  to_array_type(ns.follow(expr.type()));
298 
299  range_spect sub_size=
301 
302  if(sub_size==-1)
303  {
304  forall_operands(it, expr)
305  get_objects_rec(mode, *it, 0, -1);
306 
307  return;
308  }
309 
310  range_spect offset=0;
311  range_spect full_r_s=range_start==-1 ? 0 : range_start;
312  range_spect full_r_e=
313  size==-1 ? sub_size*expr.operands().size() : full_r_s+size;
314 
315  forall_operands(it, expr)
316  {
317  if(full_r_s<=offset+sub_size && full_r_e>offset)
318  {
319  range_spect cur_r_s=full_r_s<=offset ? 0 : full_r_s-offset;
320  range_spect cur_r_e=
321  full_r_e>offset+sub_size ? sub_size : full_r_e-offset;
322 
323  get_objects_rec(mode, *it, cur_r_s, cur_r_e-cur_r_s);
324  }
325 
326  offset+=sub_size;
327  }
328 }
329 
331  get_modet mode,
332  const struct_exprt &expr,
333  const range_spect &range_start,
334  const range_spect &size)
335 {
336  const struct_typet &struct_type=
337  to_struct_type(ns.follow(expr.type()));
338 
339  range_spect full_size=
340  to_range_spect(pointer_offset_bits(struct_type, ns));
341 
342  range_spect offset=0;
343  range_spect full_r_s=range_start==-1 ? 0 : range_start;
344  range_spect full_r_e=size==-1 || full_size==-1 ? -1 : full_r_s+size;
345 
346  forall_operands(it, expr)
347  {
348  range_spect sub_size=
349  to_range_spect(pointer_offset_bits(it->type(), ns));
350 
351  if(offset==-1)
352  {
353  get_objects_rec(mode, *it, 0, sub_size);
354  }
355  else if(sub_size==-1)
356  {
357  if(full_r_e==-1 || full_r_e>offset)
358  {
359  range_spect cur_r_s=full_r_s<=offset ? 0 : full_r_s-offset;
360 
361  get_objects_rec(mode, *it, cur_r_s, -1);
362  }
363 
364  offset=-1;
365  }
366  else if(full_r_e==-1)
367  {
368  if(full_r_s<=offset+sub_size)
369  {
370  range_spect cur_r_s=full_r_s<=offset ? 0 : full_r_s-offset;
371 
372  get_objects_rec(mode, *it, cur_r_s, sub_size-cur_r_s);
373  }
374 
375  offset+=sub_size;
376  }
377  else if(full_r_s<=offset+sub_size && full_r_e>offset)
378  {
379  range_spect cur_r_s=full_r_s<=offset ? 0 : full_r_s-offset;
380  range_spect cur_r_e=
381  full_r_e>offset+sub_size ? sub_size : full_r_e-offset;
382 
383  get_objects_rec(mode, *it, cur_r_s, cur_r_e-cur_r_s);
384 
385  offset+=sub_size;
386  }
387  }
388 }
389 
391  get_modet mode,
392  const typecast_exprt &tc,
393  const range_spect &range_start,
394  const range_spect &size)
395 {
396  const exprt &op=tc.op();
397 
398  range_spect new_size=
400 
401  if(range_start==-1)
402  new_size=-1;
403  else if(new_size!=-1)
404  {
405  if(new_size<=range_start)
406  return;
407 
408  new_size-=range_start;
409  new_size=std::min(size, new_size);
410  }
411 
412  get_objects_rec(mode, op, range_start, new_size);
413 }
414 
416 {
417  if(object.id() == ID_string_constant ||
418  object.id() == ID_label ||
419  object.id() == ID_array ||
420  object.id() == ID_null_object)
421  // constant, nothing to do
422  return;
423  else if(object.id()==ID_symbol)
425  else if(object.id()==ID_dereference)
427  else if(object.id()==ID_index)
428  {
429  const index_exprt &index=to_index_expr(object);
430 
433  }
434  else if(object.id()==ID_member)
435  {
436  const member_exprt &member=to_member_expr(object);
437 
439  }
440  else if(object.id()==ID_if)
441  {
442  const if_exprt &if_expr=to_if_expr(object);
443 
447  }
448  else if(object.id()==ID_byte_extract_little_endian ||
449  object.id()==ID_byte_extract_big_endian)
450  {
451  const byte_extract_exprt &be=to_byte_extract_expr(object);
452 
454  }
455  else if(object.id()==ID_typecast)
456  {
457  const typecast_exprt &tc=to_typecast_expr(object);
458 
460  }
461  else
462  throw "rw_range_sett: address_of `"+object.id_string()+"' not handled";
463 }
464 
466  get_modet mode,
467  const irep_idt &identifier,
468  const range_spect &range_start,
469  const range_spect &range_end)
470 {
471  objectst::iterator entry=
473  .insert(
474  std::pair<const irep_idt &, std::unique_ptr<range_domain_baset>>(
475  identifier, nullptr))
476  .first;
477 
478  if(entry->second==nullptr)
479  entry->second=util_make_unique<range_domaint>();
480 
481  static_cast<range_domaint&>(*entry->second).push_back(
482  {range_start, range_end});
483 }
484 
486  get_modet mode,
487  const exprt &expr,
488  const range_spect &range_start,
489  const range_spect &size)
490 {
491  if(expr.id()==ID_complex_real ||
492  expr.id()==ID_complex_imag)
493  get_objects_complex(mode, expr, range_start, size);
494  else if(expr.id()==ID_typecast)
496  mode,
497  to_typecast_expr(expr),
498  range_start,
499  size);
500  else if(expr.id()==ID_if)
501  get_objects_if(mode, to_if_expr(expr), range_start, size);
502  else if(expr.id()==ID_dereference)
504  mode,
505  to_dereference_expr(expr),
506  range_start,
507  size);
508  else if(expr.id()==ID_byte_extract_little_endian ||
509  expr.id()==ID_byte_extract_big_endian)
511  mode,
512  to_byte_extract_expr(expr),
513  range_start,
514  size);
515  else if(expr.id()==ID_shl ||
516  expr.id()==ID_ashr ||
517  expr.id()==ID_lshr)
518  get_objects_shift(mode, to_shift_expr(expr), range_start, size);
519  else if(expr.id()==ID_member)
520  get_objects_member(mode, to_member_expr(expr), range_start, size);
521  else if(expr.id()==ID_index)
522  get_objects_index(mode, to_index_expr(expr), range_start, size);
523  else if(expr.id()==ID_array)
524  get_objects_array(mode, to_array_expr(expr), range_start, size);
525  else if(expr.id()==ID_struct)
526  get_objects_struct(mode, to_struct_expr(expr), range_start, size);
527  else if(expr.id()==ID_symbol)
528  {
529  const symbol_exprt &symbol=to_symbol_expr(expr);
530  const irep_idt identifier=symbol.get_identifier();
531  range_spect full_size=
533 
534  if(full_size==0 ||
535  (full_size>0 && range_start>=full_size))
536  {
537  // nothing to do, these are effectively constants (like function
538  // symbols or structs with no members)
539  // OR: invalid memory accesses
540  }
541  else if(range_start>=0)
542  {
543  range_spect range_end=size==-1 ? -1 : range_start+size;
544  if(size!=-1 && full_size!=-1)
545  range_end=std::max(range_end, full_size);
546 
547  add(mode, identifier, range_start, range_end);
548  }
549  else
550  add(mode, identifier, 0, -1);
551  }
552  else if(mode==get_modet::READ && expr.id()==ID_address_of)
554  else if(mode==get_modet::READ)
555  {
556  // possibly affects the full object size, even if range_start/size
557  // are only a subset of the bytes (e.g., when using the result of
558  // arithmetic operations)
559  forall_operands(it, expr)
560  get_objects_rec(mode, *it);
561  }
562  else if(expr.id() == ID_null_object ||
563  expr.id() == ID_string_constant)
564  {
565  // dereferencing may yield some weird ones, ignore these
566  }
567  else if(mode==get_modet::LHS_W)
568  {
569  forall_operands(it, expr)
570  get_objects_rec(mode, *it);
571  }
572  else
573  throw "rw_range_sett: assignment to `"+expr.id_string()+"' not handled";
574 }
575 
577 {
578  range_spect size=
580  get_objects_rec(mode, expr, 0, size);
581 }
582 
584 {
585  // TODO should recurse into various composite types
586  if(type.id()==ID_array)
587  {
588  get_objects_rec(type.subtype());
590  }
591 }
592 
594  get_modet mode,
595  const dereference_exprt &deref,
596  const range_spect &range_start,
597  const range_spect &size)
598 {
600  mode,
601  deref,
602  range_start,
603  size);
604 
605  exprt object=deref;
606  dereference(target, object, ns, value_sets);
607 
608  range_spect new_size=
609  to_range_spect(pointer_offset_bits(object.type(), ns));
610 
611  if(range_start==-1 || new_size<=range_start)
612  new_size=-1;
613  else
614  {
615  new_size-=range_start;
616  new_size=std::min(size, new_size);
617  }
618 
619  // value_set_dereferencet::build_reference_to will turn *p into
620  // DYNAMIC_OBJECT(p) ? *p : invalid_objectN
621  if(object.is_not_nil() && !has_subexpr(object, ID_dereference))
622  get_objects_rec(mode, object, range_start, new_size);
623 }
624 
626  const namespacet &ns, std::ostream &out) const
627 {
628  out << "[";
629  for(const_iterator itr=begin();
630  itr!=end();
631  ++itr)
632  {
633  if(itr!=begin())
634  out << ";";
635  out << itr->first << ":" << itr->second.first;
636  // we don't know what mode (language) we are in, so we rely on the default
637  // language to be reasonable for from_expr
638  out << " if " << from_expr(ns, "", itr->second.second);
639  }
640  out << "]";
641 }
642 
644  get_modet mode,
645  const if_exprt &if_expr,
646  const range_spect &range_start,
647  const range_spect &size)
648 {
649  if(if_expr.cond().is_false())
650  get_objects_rec(mode, if_expr.false_case(), range_start, size);
651  else if(if_expr.cond().is_true())
652  get_objects_rec(mode, if_expr.true_case(), range_start, size);
653  else
654  {
656 
657  guardt guard_bak1(guard), guard_bak2(guard);
658 
659  guard.add(not_exprt(if_expr.cond()));
660  get_objects_rec(mode, if_expr.false_case(), range_start, size);
661  guard.swap(guard_bak1);
662 
663  guard.add(if_expr.cond());
664  get_objects_rec(mode, if_expr.true_case(), range_start, size);
665  guard.swap(guard_bak2);
666  }
667 }
668 
670  get_modet mode,
671  const irep_idt &identifier,
672  const range_spect &range_start,
673  const range_spect &range_end)
674 {
675  objectst::iterator entry=
677  .insert(
678  std::pair<const irep_idt &, std::unique_ptr<range_domain_baset>>(
679  identifier, nullptr))
680  .first;
681 
682  if(entry->second==nullptr)
683  entry->second=util_make_unique<guarded_range_domaint>();
684 
685  static_cast<guarded_range_domaint&>(*entry->second).insert(
686  {range_start, {range_end, guard.as_expr()}});
687 }
688 
690  const code_assignt &assign,
691  rw_range_sett &rw_set)
692 {
693  rw_set.get_objects_rec(target, rw_range_sett::get_modet::LHS_W, assign.lhs());
694  rw_set.get_objects_rec(target, rw_range_sett::get_modet::READ, assign.rhs());
695 }
696 
698  const code_function_callt &function_call,
699  rw_range_sett &rw_set)
700 {
701  if(function_call.lhs().is_not_nil())
702  rw_set.get_objects_rec(
703  target,
705  function_call.lhs());
706 
707  rw_set.get_objects_rec(
708  target,
710  function_call.function());
711 
712  forall_expr(it, function_call.arguments())
713  rw_set.get_objects_rec(target, rw_range_sett::get_modet::READ, *it);
714 }
715 
717  rw_range_sett &rw_set)
718 {
719  switch(target->type)
720  {
721  case NO_INSTRUCTION_TYPE:
722  case INCOMPLETE_GOTO:
723  UNREACHABLE;
724  break;
725 
726  case GOTO:
727  case ASSUME:
728  case ASSERT:
729  rw_set.get_objects_rec(
730  target,
732  target->guard);
733  break;
734 
735  case RETURN:
736  {
737  const code_returnt &code_return=
738  to_code_return(target->code);
739  if(code_return.has_return_value())
740  rw_set.get_objects_rec(
741  target,
743  code_return.return_value());
744  }
745  break;
746 
747  case OTHER:
748  // if it's printf, mark the operands as read here
749  if(target->code.get(ID_statement)==ID_printf)
750  {
751  forall_expr(it, target->code.operands())
752  rw_set.get_objects_rec(target, rw_range_sett::get_modet::READ, *it);
753  }
754  break;
755 
756  case SKIP:
757  case START_THREAD:
758  case END_THREAD:
759  case LOCATION:
760  case END_FUNCTION:
761  case ATOMIC_BEGIN:
762  case ATOMIC_END:
763  case THROW:
764  case CATCH:
765  // these don't read or write anything
766  break;
767 
768  case ASSIGN:
769  goto_rw(target, to_code_assign(target->code), rw_set);
770  break;
771 
772  case DEAD:
773  rw_set.get_objects_rec(
774  target,
776  to_code_dead(target->code).symbol());
777  break;
778 
779  case DECL:
780  rw_set.get_objects_rec(
781  to_code_decl(target->code).symbol().type());
782  rw_set.get_objects_rec(
783  target,
785  to_code_decl(target->code).symbol());
786  break;
787 
788  case FUNCTION_CALL:
789  goto_rw(target, to_code_function_call(target->code), rw_set);
790  break;
791  }
792 }
793 
795 {
797  goto_rw(i_it, rw_set);
798 }
799 
800 void goto_rw(const goto_functionst &goto_functions,
801  const irep_idt &function,
802  rw_range_sett &rw_set)
803 {
804  goto_functionst::function_mapt::const_iterator f_it=
805  goto_functions.function_map.find(function);
806 
807  if(f_it!=goto_functions.function_map.end())
808  {
809  const goto_programt &body=f_it->second.body;
810 
811  goto_rw(body, rw_set);
812  }
813 }
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
Definition: std_expr.h:3426
virtual void get_objects_rec(goto_programt::const_targett _target, get_modet mode, const exprt &expr)
Definition: goto_rw.h:143
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:907
Boolean negation.
Definition: std_expr.h:3230
const code_declt & to_code_decl(const codet &code)
Definition: std_code.h:289
exprt & true_case()
Definition: std_expr.h:3395
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:103
Maps a big-endian offset to a little-endian offset.
exprt & object()
Definition: std_expr.h:3180
#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:341
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:266
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:52
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:593
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:210
The trinary if-then-else operator.
Definition: std_expr.h:3361
exprt & cond()
Definition: std_expr.h:3385
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:240
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:86
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:3201
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:330
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:3328
iterator end()
Definition: goto_rw.h:90
Extract member of struct or union.
Definition: std_expr.h:3871
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:643
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:239
const irep_idt & id() const
Definition: irep.h:189
exprt & lhs()
Definition: std_code.h:208
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:860
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:415
virtual void add(get_modet mode, const irep_idt &identifier, const range_spect &range_start, const range_spect &range_end)
Definition: goto_rw.cpp:465
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:125
exprt & rhs()
Definition: std_code.h:213
Operator to dereference a pointer.
Definition: std_expr.h:3284
A constant-size array type.
Definition: std_types.h:1629
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:135
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:104
void goto_rw(goto_programt::const_targett target, const code_assignt &assign, rw_range_sett &rw_set)
Definition: goto_rw.cpp:689
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
Definition: std_expr.h:3955
const code_returnt & to_code_return(const codet &code)
Definition: std_code.h:933
const vector_typet & to_vector_type(const typet &type)
Cast a generic typet to a vector_typet.
Definition: std_types.h:1660
A function call.
Definition: std_code.h:828
#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
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:162
Operator to return the address of an object.
Definition: std_expr.h:3170
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:318
exprt & false_case()
Definition: std_expr.h:3405
virtual void add(get_modet mode, const irep_idt &identifier, const range_spect &range_start, const range_spect &range_end)
Definition: goto_rw.cpp:669
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:290
bool has_return_value() const
Definition: std_code.h:917
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:390
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:123
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:848
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Definition: std_types.h:1045
Base class for all expressions.
Definition: expr.h:42
exprt & pointer()
Definition: std_expr.h:3307
const exprt & struct_op() const
Definition: std_expr.h:3911
irep_idt get_component_name() const
Definition: std_expr.h:3895
#define UNREACHABLE
Definition: invariant.h:250
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:625
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:192
void swap(irept &irep)
Definition: irep.h:231
goto_programt & goto_program
Definition: cover.cpp:63
arrays with given size
Definition: std_types.h:1004
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:893
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:65
array constructor from list of elements
Definition: std_expr.h:1617
Assignment.
Definition: std_code.h:195
void add(const exprt &expr)
Definition: guard.cpp:64
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:879
iterator begin()
Definition: goto_rw.h:86
array index operator
Definition: std_expr.h:1462