CBMC
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 "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 
28 }
Base class for all expressions.
Definition: expr.h:56
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
const irep_idt & id() const
Definition: irep.h:388
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
exprt pointer_offset_sum(const exprt &a, const exprt &b)
Pointer Dereferencing.
API to expression classes.