CBMC
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/pointer_expr.h>
13 #include <util/std_expr.h>
14 
16 {
17  pointer.make_nil();
18  offset.make_nil();
19  read(src);
20 }
21 
23 {
24  if(src.id()==ID_plus)
25  {
26  for(const auto &op : src.operands())
27  {
28  if(op.type().id() == ID_pointer)
29  read(op);
30  else
31  add_to_offset(op);
32  }
33  }
34  else if(src.id()==ID_minus)
35  {
36  auto const &minus_src = to_minus_expr(src);
37  read(minus_src.op0());
38  const unary_minus_exprt unary_minus(
39  minus_src.op1(), minus_src.op1().type());
40  add_to_offset(unary_minus);
41  }
42  else if(src.id()==ID_address_of)
43  {
44  auto const &address_of_src = to_address_of_expr(src);
45  if(address_of_src.op().id() == ID_index)
46  {
47  const index_exprt &index_expr = to_index_expr(address_of_src.op());
48 
49  if(index_expr.index().is_zero())
50  make_pointer(address_of_src);
51  else
52  {
53  add_to_offset(index_expr.index());
54  // produce &x[0] + i instead of &x[i]
55  auto new_address_of_src = address_of_src;
56  to_index_expr(new_address_of_src.op()).index() =
57  from_integer(0, index_expr.index().type());
58  make_pointer(new_address_of_src);
59  }
60  }
61  else
62  make_pointer(address_of_src);
63  }
64  else
65  make_pointer(src);
66 }
67 
69 {
70  if(offset.is_nil())
71  offset=src;
72  else if(offset.id()==ID_plus)
74  else
75  {
76  offset =
78  }
79 }
80 
82 {
83  if(pointer.is_nil())
84  pointer=src;
85  else
86  add_to_offset(src);
87 }
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
Base class for all expressions.
Definition: expr.h:56
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
Definition: expr.h:163
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:47
typet & type()
Return the type of the expression.
Definition: expr.h:84
operandst & operands()
Definition: expr.h:94
Array index operator.
Definition: std_expr.h:1470
exprt & index()
Definition: std_expr.h:1510
const irep_idt & id() const
Definition: irep.h:388
void make_nil()
Definition: irep.h:446
bool is_nil() const
Definition: irep.h:368
The plus expression Associativity is not specified.
Definition: std_expr.h:1002
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:2081
The unary minus expression.
Definition: std_expr.h:484
API to expression classes for Pointers.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:577
API to expression classes.
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
Definition: std_expr.h:1086
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1538
void make_pointer(const exprt &src)
void add_to_offset(const exprt &src)
void read(const exprt &src)
pointer_arithmetict(const exprt &src)