CBMC
array_element_from_pointer.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Element access in a pointer array
4 
5 Author: Diffblue Ltd.
6 
7 \*******************************************************************/
8 
9 #ifndef CPROVER_UTIL_ARRAY_ELEMENT_FROM_POINTER_H
10 #define CPROVER_UTIL_ARRAY_ELEMENT_FROM_POINTER_H
11 
12 #include "pointer_expr.h"
13 
24 dereference_exprt
25 array_element_from_pointer(const exprt &pointer, const exprt &index);
26 
27 #endif // CPROVER_UTIL_ARRAY_ELEMENT_FROM_POINTER_H
array_element_from_pointer
dereference_exprt array_element_from_pointer(const exprt &pointer, const exprt &index)
Generate statement using pointer arithmetic to access the element at the given index of a pointer arr...
Definition: array_element_from_pointer.cpp:12
dereference_exprt
Operator to dereference a pointer.
Definition: pointer_expr.h:834
exprt
Base class for all expressions.
Definition: expr.h:56
pointer_expr.h
API to expression classes for Pointers.