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.

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: pointer pointer to the first element of an array

index index 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.