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

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.