cprover
Loading...
Searching...
No Matches
array_element_from_pointer.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Element access in a pointer array
4
5Author: Diffblue Ltd.
6
7\*******************************************************************/
8
10
12array_element_from_pointer(const exprt &pointer, const exprt &index)
13{
16 index.type().id() == ID_signedbv || index.type().id() == ID_unsignedbv);
17 return dereference_exprt{plus_exprt{pointer, index}};
18}
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...
Operator to dereference a pointer.
Base class for all expressions.
Definition expr.h:54
typet & type()
Return the type of the expression.
Definition expr.h:82
const irep_idt & id() const
Definition irep.h:396
The plus expression Associativity is not specified.
Definition std_expr.h:914
bool can_cast_type< pointer_typet >(const typet &type)
Check whether a reference to a typet is a pointer_typet.
#define PRECONDITION(CONDITION)
Definition invariant.h:463