cprover
pointer_arithmetic.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "pointer_arithmetic.h"
10 
11 #include <util/arith_tools.h>
12 #include <util/std_expr.h>
13 
15 {
16  pointer.make_nil();
17  offset.make_nil();
18  read(src);
19 }
20 
22 {
23  if(src.id()==ID_plus)
24  {
25  forall_operands(it, src)
26  {
27  if(it->type().id()==ID_pointer)
28  read(*it);
29  else
30  add_to_offset(*it);
31  }
32  }
33  else if(src.id()==ID_minus)
34  {
35  assert(src.operands().size()==2);
36  read(src.op0());
37  const unary_minus_exprt o(src.op1(), src.op1().type());
38  add_to_offset(o);
39  }
40  else if(src.id()==ID_address_of)
41  {
42  assert(src.operands().size()==1);
43  if(src.op0().id()==ID_index)
44  {
45  const index_exprt &index_expr=
46  to_index_expr(src.op0());
47 
48  if(index_expr.index().is_zero())
49  make_pointer(src);
50  else
51  {
52  add_to_offset(index_expr.index());
53  // produce &x[0] + i instead of &x[i]
54  exprt new_src=src;
55  new_src.op0().op1()=from_integer(0, index_expr.index().type());
56  make_pointer(new_src);
57  }
58  }
59  else
60  make_pointer(src);
61  }
62  else
63  make_pointer(src);
64 }
65 
67 {
68  if(offset.is_nil())
69  offset=src;
70  else if(offset.id()==ID_plus)
72  else
73  {
74  exprt new_offset=plus_exprt(offset, src);
75 
76  if(new_offset.op1().type()!=offset.type())
77  new_offset.op1().make_typecast(offset.type());
78 
79  offset=new_offset;
80  }
81 }
82 
84 {
85  if(pointer.is_nil())
86  pointer=src;
87  else
88  add_to_offset(src);
89 }
bool is_nil() const
Definition: irep.h:102
exprt & op0()
Definition: expr.h:72
void copy_to_operands(const exprt &expr)
Definition: expr.cpp:55
typet & type()
Definition: expr.h:56
const irep_idt & id() const
Definition: irep.h:189
void add_to_offset(const exprt &src)
API to expression classes.
exprt & op1()
Definition: expr.h:75
pointer_arithmetict(const exprt &src)
#define forall_operands(it, expr)
Definition: expr.h:17
The plus expression.
Definition: std_expr.h:893
void read(const exprt &src)
void make_pointer(const exprt &src)
The unary minus expression.
Definition: std_expr.h:444
exprt & index()
Definition: std_expr.h:1496
Base class for all expressions.
Definition: expr.h:42
void make_nil()
Definition: irep.h:243
bool is_zero() const
Definition: expr.cpp:161
operandst & operands()
Definition: expr.h:66
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
void make_typecast(const typet &_type)
Definition: expr.cpp:84
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
Definition: std_expr.h:1517
array index operator
Definition: std_expr.h:1462