cprover
rewrite_index.cpp
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module: Pointer Dereferencing
4
5
Author: Daniel Kroening, kroening@kroening.com
6
7
\*******************************************************************/
8
11
12
#include "
rewrite_index.h
"
13
14
#include <
util/std_expr.h
>
15
17
dereference_exprt
rewrite_index
(
const
index_exprt
&index_expr)
18
{
19
dereference_exprt
result;
20
result.
pointer
()=
plus_exprt
(index_expr.
array
(), index_expr.
index
());
21
result.
type
()=index_expr.
type
();
22
result.
add_source_location
()=index_expr.
source_location
();
23
return
result;
24
}
rewrite_index
dereference_exprt rewrite_index(const index_exprt &index_expr)
rewrite a[i] to *(a+i)
Definition:
rewrite_index.cpp:17
exprt::type
typet & type()
Definition:
expr.h:56
rewrite_index.h
Pointer Dereferencing.
dereference_exprt
Operator to dereference a pointer.
Definition:
std_expr.h:3282
std_expr.h
API to expression classes.
plus_exprt
The plus expression.
Definition:
std_expr.h:893
index_exprt::index
exprt & index()
Definition:
std_expr.h:1496
dereference_exprt::pointer
exprt & pointer()
Definition:
std_expr.h:3305
exprt::source_location
const source_locationt & source_location() const
Definition:
expr.h:125
exprt::add_source_location
source_locationt & add_source_location()
Definition:
expr.h:130
index_exprt::array
exprt & array()
Definition:
std_expr.h:1486
index_exprt
array index operator
Definition:
std_expr.h:1462
pointer-analysis
rewrite_index.cpp
Generated by
1.8.14