CBMC
Loading...
Searching...
No Matches
pointer_arithmetic.h
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module:
4
5
Author: 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
15
struct
pointer_arithmetict
16
{
17
exprt
pointer
,
offset
;
18
19
explicit
pointer_arithmetict
(
const
exprt
&src);
20
21
protected
:
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
exprt
Base class for all expressions.
Definition
expr.h:56
expr.h
read
int __CPROVER_ID java::java io InputStream read
Definition
java.io.c:5
pointer_arithmetict
Definition
pointer_arithmetic.h:16
pointer_arithmetict::pointer
exprt pointer
Definition
pointer_arithmetic.h:17
pointer_arithmetict::make_pointer
void make_pointer(const exprt &src)
Definition
pointer_arithmetic.cpp:81
pointer_arithmetict::add_to_offset
void add_to_offset(const exprt &src)
Definition
pointer_arithmetic.cpp:68
pointer_arithmetict::offset
exprt offset
Definition
pointer_arithmetic.h:17
src
goto-programs
pointer_arithmetic.h
Generated by
1.9.8