CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
pointer_offset_sum.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Pointer Dereferencing
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#ifndef CPROVER_UTIL_POINTER_OFFSET_SUM_H
13#define CPROVER_UTIL_POINTER_OFFSET_SUM_H
14
15#include "expr.h"
16
17exprt pointer_offset_sum(const exprt &a, const exprt &b);
18
19#endif // CPROVER_UTIL_POINTER_OFFSET_SUM_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Base class for all expressions.
Definition expr.h:56
exprt pointer_offset_sum(const exprt &a, const exprt &b)