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 #include <util/std_expr.h>
15 
16 exprt pointer_offset_sum(const exprt &a, const exprt &b)
17 {
18  if(a.id()==ID_unknown)
19  return a;
20  else if(b.id()==ID_unknown)
21  return b;
22  else if(a.is_zero())
23  return b;
24  else if(b.is_zero())
25  return a;
26 
27  plus_exprt new_offset(a, b);
28 
29  if(b.type() != a.type())
30  new_offset.op1().make_typecast(a.type());
31 
32  return new_offset;
33 }
Pointer Dereferencing.
typet & type()
Definition: expr.h:56
exprt pointer_offset_sum(const exprt &a, const exprt &b)
const irep_idt & id() const
Definition: irep.h:259
API to expression classes.
exprt & op1()
Definition: expr.h:75
The plus expression.
Definition: std_expr.h:893
Base class for all expressions.
Definition: expr.h:42
bool is_zero() const
Definition: expr.cpp:161
void make_typecast(const typet &_type)
Definition: expr.cpp:84