CBMC: /home/runner/work/cbmc/cbmc/src/goto-programs/pointer_arithmetic.h Source File

CBMC
Loading...
Searching...
No Matches
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:57
int __CPROVER_ID java::java io InputStream read
Definition java.io.c:5
exprt pointer
void make_pointer(const exprt &src)
void add_to_offset(const exprt &src)
exprt offset

AltStyle によって変換されたページ (->オリジナル) /