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  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 }
dereference_exprt rewrite_index(const index_exprt &index_expr)
rewrite a[i] to *(a+i)
typet & type()
Definition: expr.h:56
Pointer Dereferencing.
Operator to dereference a pointer.
Definition: std_expr.h:3282
API to expression classes.
The plus expression.
Definition: std_expr.h:893
exprt & index()
Definition: std_expr.h:1496
exprt & pointer()
Definition: std_expr.h:3305
const source_locationt & source_location() const
Definition: expr.h:125
source_locationt & add_source_location()
Definition: expr.h:130
exprt & array()
Definition: std_expr.h:1486
array index operator
Definition: std_expr.h:1462