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, typecast_exprt::conditional_cast(b, a.type()));
28  return std::move(new_offset);
29 }
Pointer Dereferencing.
typet & type()
Return the type of the expression.
Definition: expr.h:68
exprt pointer_offset_sum(const exprt &a, const exprt &b)
const irep_idt & id() const
Definition: irep.h:259
API to expression classes.
The plus expression Associativity is not specified.
Definition: std_expr.h:1042
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:2291
Base class for all expressions.
Definition: expr.h:54
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:130