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}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
Operator to dereference a pointer.
source_locationt & add_source_location()
Definition expr.h:235
Array index operator.
Definition std_expr.h:1328
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.