cprover
Loading...
Searching...
No Matches
rewrite_index.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Pointer Dereferencing
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#include "rewrite_index.h"
13
14#include <util/pointer_expr.h>
15#include <util/std_expr.h>
16
19{
20 dereference_exprt result(
21 plus_exprt(index_expr.array(), index_expr.index()), index_expr.type());
22 result.add_source_location()=index_expr.source_location();
23 return result;
24}
Operator to dereference a pointer.
typet & type()
Return the type of the expression.
Definition expr.h:82
const source_locationt & source_location() const
Definition expr.h:230
source_locationt & add_source_location()
Definition expr.h:235
Array index operator.
Definition std_expr.h:1328
exprt & index()
Definition std_expr.h:1363
exprt & array()
Definition std_expr.h:1353
The plus expression Associativity is not specified.
Definition std_expr.h:914
API to expression classes for Pointers.
dereference_exprt rewrite_index(const index_exprt &index_expr)
rewrite a[i] to *(a+i)
Pointer Dereferencing.
API to expression classes.