CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
pointer_arithmetic.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9
10#ifndef CPROVER_GOTO_PROGRAMS_POINTER_ARITHMETIC_H
11#define CPROVER_GOTO_PROGRAMS_POINTER_ARITHMETIC_H
12
13#include <util/expr.h>
14
16{
18
19 explicit pointer_arithmetict(const exprt &src);
20
21protected:
22 void read(const exprt &src);
23 void add_to_offset(const exprt &src);
24 void make_pointer(const exprt &src);
25};
26
27#endif // CPROVER_GOTO_PROGRAMS_POINTER_ARITHMETIC_H
Base class for all expressions.
Definition expr.h:56
int __CPROVER_ID java::java io InputStream read
Definition java.io.c:5
void make_pointer(const exprt &src)
void add_to_offset(const exprt &src)