cprover
pointer_offset_sum.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Pointer Analysis
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "pointer_offset_sum.h"
13 
14 exprt pointer_offset_sum(const exprt &a, const exprt &b)
15 {
16  if(a.id()==ID_unknown)
17  return a;
18  else if(b.id()==ID_unknown)
19  return b;
20  else if(a.is_zero())
21  return b;
22  else if(b.is_zero())
23  return a;
24 
25  exprt new_offset(ID_plus, a.type());
26  new_offset.copy_to_operands(a, b);
27 
28  if(new_offset.op1().type()!=a.type())
29  new_offset.op1().make_typecast(a.type());
30 
31  return new_offset;
32 }
Pointer Dereferencing.
void copy_to_operands(const exprt &expr)
Definition: expr.cpp:61
typet & type()
Definition: expr.h:60
exprt pointer_offset_sum(const exprt &a, const exprt &b)
const irep_idt & id() const
Definition: irep.h:189
Base class for all expressions.
Definition: expr.h:46
bool is_zero() const
Definition: expr.cpp:236