CBMC
array_element_from_pointer.cpp
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 #include "array_element_from_pointer.h"
10 
11 dereference_exprt
12 array_element_from_pointer(const exprt &pointer, const exprt &index)
13 {
14  PRECONDITION(can_cast_type<pointer_typet>(pointer.type()));
15  PRECONDITION(
16  index.type().id() == ID_signedbv || index.type().id() == ID_unsignedbv);
17  return dereference_exprt{plus_exprt{pointer, index}};
18 }
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
array_element_from_pointer.h
dereference_exprt
Operator to dereference a pointer.
Definition: pointer_expr.h:834
exprt
Base class for all expressions.
Definition: expr.h:56
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:84
irept::id
const irep_idt & id() const
Definition: irep.h:384
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:1002
can_cast_type< pointer_typet >
bool can_cast_type< pointer_typet >(const typet &type)
Check whether a reference to a typet is a pointer_typet.
Definition: pointer_expr.h:80
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:463