CBMC
rewrite_index.h
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 #ifndef CPROVER_POINTER_ANALYSIS_REWRITE_INDEX_H
13 #define CPROVER_POINTER_ANALYSIS_REWRITE_INDEX_H
14 
15 #include <util/deprecate.h>
16 
17 class dereference_exprt;
18 class index_exprt;
19 
20 // rewrite a[i] to *(a+i)
21 DEPRECATED(SINCE(2022, 07, 23, "implement the transform directly"))
22 dereference_exprt rewrite_index(const index_exprt &index_expr);
23 
24 #endif // CPROVER_POINTER_ANALYSIS_REWRITE_INDEX_H
dereference_exprt
Operator to dereference a pointer.
Definition: pointer_expr.h:659
deprecate.h
SINCE
#define SINCE(year, month, day, msg)
Definition: deprecate.h:26
DEPRECATED
#define DEPRECATED(msg)
Definition: deprecate.h:23
rewrite_index
dereference_exprt rewrite_index(const index_exprt &index_expr)
rewrite a[i] to *(a+i)
Definition: rewrite_index.cpp:18
index_exprt
Array index operator.
Definition: std_expr.h:1409