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
plus_exprt
(index_expr.
array
(), index_expr.
index
()), index_expr.
type
());
21
result.
add_source_location
()=index_expr.
source_location
();
22
return
result;
23
}
rewrite_index.h
Pointer Dereferencing.
dereference_exprt
Operator to dereference a pointer.
Definition:
std_expr.h:2888
plus_exprt
The plus expression Associativity is not specified.
Definition:
std_expr.h:881
exprt::type
typet & type()
Return the type of the expression.
Definition:
expr.h:81
index_exprt::index
exprt & index()
Definition:
std_expr.h:1319
index_exprt::array
exprt & array()
Definition:
std_expr.h:1309
rewrite_index
dereference_exprt rewrite_index(const index_exprt &index_expr)
rewrite a[i] to *(a+i)
Definition:
rewrite_index.cpp:17
index_exprt
Array index operator.
Definition:
std_expr.h:1293
exprt::add_source_location
source_locationt & add_source_location()
Definition:
expr.h:259
std_expr.h
API to expression classes.
exprt::source_location
const source_locationt & source_location() const
Definition:
expr.h:254
pointer-analysis
rewrite_index.cpp
Generated by
1.8.20