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_offset_sum.h
Pointer Dereferencing.
exprt::type
typet & type()
Definition:
expr.h:56
pointer_offset_sum
exprt pointer_offset_sum(const exprt &a, const exprt &b)
Definition:
pointer_offset_sum.cpp:16
irept::id
const irep_idt & id() const
Definition:
irep.h:259
std_expr.h
API to expression classes.
exprt::op1
exprt & op1()
Definition:
expr.h:75
plus_exprt
The plus expression.
Definition:
std_expr.h:893
exprt
Base class for all expressions.
Definition:
expr.h:42
exprt::is_zero
bool is_zero() const
Definition:
expr.cpp:161
exprt::make_typecast
void make_typecast(const typet &_type)
Definition:
expr.cpp:84
pointer-analysis
pointer_offset_sum.cpp
Generated by
1.8.14