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