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 
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