CBMC
array_element_from_pointer.h File Reference
#include "pointer_expr.h"
+ Include dependency graph for array_element_from_pointer.h:
+ This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Functions

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 array: *(pointer + index) Arrays are sometimes (always in JBMC) represented as a pointer to their first element, especially when their length in uncertain, as the length is part of any array type. More...
 

Function Documentation

◆ 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 array: *(pointer + index) Arrays are sometimes (always in JBMC) represented as a pointer to their first element, especially when their length in uncertain, as the length is part of any array type.

But we know the type of the first element of the array, so we work with that instead.

Parameters
pointerpointer to the first element of an array
indexindex of the element to access
Returns
expression representing the (index)'th element of the array

Definition at line 12 of file array_element_from_pointer.cpp.