CBMC: /home/runner/work/cbmc/cbmc/src/ansi-c/library/fcntl.c Source File

CBMC
Loading...
Searching...
No Matches
fcntl.c
Go to the documentation of this file.
1/* FUNCTION: __CPROVER_fcntl */
2
3#ifndef __CPROVER_FCNTL_H_INCLUDED
4#include <fcntl.h>
5 #define __CPROVER_FCNTL_H_INCLUDED
6#endif
7
8#ifndef __CPROVER_ERRNO_H_INCLUDED
9# include <errno.h>
10 # define __CPROVER_ERRNO_H_INCLUDED
11#endif
12
13 int __VERIFIER_nondet_int(void);
14
15 int __CPROVER_fcntl(int fd, int cmd)
16{
18 if(fd < 0)
19 {
20 errno = EBADF;
21 return -1;
22 }
23
24 int return_value=__VERIFIER_nondet_int();
25 (void)fd;
26 (void)cmd;
27 return return_value;
28}
29
30/* FUNCTION: fcntl */
31
32int __CPROVER_fcntl(int, int);
33
34 int fcntl(int fd, int cmd, ...)
35{
36 return __CPROVER_fcntl(fd, cmd);
37}
38
39/* FUNCTION: _fcntl */
40
41int __CPROVER_fcntl(int, int);
42
43 int _fcntl(int fd, int cmd, ...)
44{
45 return __CPROVER_fcntl(fd, cmd);
46}
47
48/* FUNCTION: fcntl64 */
49
50int __CPROVER_fcntl(int, int);
51
52 int fcntl64(int fd, int cmd, ...)
53{
54 return __CPROVER_fcntl(fd, cmd);
55}
56
57/* FUNCTION: __fcntl_time64 */
58
59int __CPROVER_fcntl(int, int);
60
61 int __fcntl_time64(int fd, int cmd, ...)
62{
63 return __CPROVER_fcntl(fd, cmd);
64}
65
66/* FUNCTION: __CPROVER_open */
67
68#ifndef __CPROVER_FCNTL_H_INCLUDED
69# include <fcntl.h>
70# define __CPROVER_FCNTL_H_INCLUDED
71#endif
72
73int __VERIFIER_nondet_int(void);
74
75 int __CPROVER_open(const char *pathname, int flags)
76{
78 int return_value = __VERIFIER_nondet_int();
79 __CPROVER_assume(return_value >= -1);
80 (void)*pathname;
81 (void)flags;
82 return return_value;
83}
84
85/* FUNCTION: open */
86
87int __CPROVER_open(const char *, int);
88
89 int open(const char *pathname, int flags, ...)
90{
91 return __CPROVER_open(pathname, flags);
92}
93
94/* FUNCTION: _open */
95
96int __CPROVER_open(const char *, int);
97
98 int _open(const char *pathname, int flags, ...)
99{
100 return __CPROVER_open(pathname, flags);
101}
102
103/* FUNCTION: open64 */
104
105int __CPROVER_open(const char *, int);
106
107 int open64(const char *pathname, int flags, ...)
108{
109 return __CPROVER_open(pathname, flags);
110}
111
112/* FUNCTION: __CPROVER_creat */
113
114#ifndef __CPROVER_FCNTL_H_INCLUDED
115# include <fcntl.h>
116# define __CPROVER_FCNTL_H_INCLUDED
117#endif
118
119#ifndef MODE_T
120# ifdef _WIN32
121# define MODE_T int
122# else
123 # define MODE_T mode_t
124# endif
125#endif
126
127int __VERIFIER_nondet_int(void);
128
129 int __CPROVER_creat(const char *pathname, MODE_T mode)
130{
132 int return_value = __VERIFIER_nondet_int();
133 __CPROVER_assume(return_value >= -1);
134 (void)*pathname;
135 (void)mode;
136 return return_value;
137}
138
139/* FUNCTION: creat */
140
141#ifndef __CPROVER_FCNTL_H_INCLUDED
142# include <fcntl.h>
143# define __CPROVER_FCNTL_H_INCLUDED
144#endif
145
146#ifndef MODE_T
147# ifdef _WIN32
148# define MODE_T int
149# else
150# define MODE_T mode_t
151# endif
152#endif
153
154int __CPROVER_creat(const char *, MODE_T);
155
156 int creat(const char *pathname, MODE_T mode)
157{
158 return __CPROVER_creat(pathname, mode);
159}
160
161/* FUNCTION: _creat */
162
163#ifndef __CPROVER_FCNTL_H_INCLUDED
164# include <fcntl.h>
165# define __CPROVER_FCNTL_H_INCLUDED
166#endif
167
168#ifndef MODE_T
169# ifdef _WIN32
170# define MODE_T int
171# else
172# define MODE_T mode_t
173# endif
174#endif
175
176int __CPROVER_creat(const char *, MODE_T);
177
178 int _creat(const char *pathname, MODE_T mode)
179{
180 return __CPROVER_creat(pathname, mode);
181}
182
183/* FUNCTION: creat64 */
184
185#ifndef __CPROVER_FCNTL_H_INCLUDED
186# include <fcntl.h>
187# define __CPROVER_FCNTL_H_INCLUDED
188#endif
189
190#ifndef MODE_T
191# ifdef _WIN32
192# define MODE_T int
193# else
194# define MODE_T mode_t
195# endif
196#endif
197
198int __CPROVER_creat(const char *, MODE_T);
199
200 int creat64(const char *pathname, MODE_T mode)
201{
202 return __CPROVER_creat(pathname, mode);
203}
204
205/* FUNCTION: __CPROVER_openat */
206
207#ifndef __CPROVER_FCNTL_H_INCLUDED
208# include <fcntl.h>
209# define __CPROVER_FCNTL_H_INCLUDED
210#endif
211
212#ifndef __CPROVER_ERRNO_H_INCLUDED
213# include <errno.h>
214# define __CPROVER_ERRNO_H_INCLUDED
215#endif
216
217int __VERIFIER_nondet_int(void);
218
219 int __CPROVER_openat(int dirfd, const char *pathname, int flags)
220{
222 if(dirfd < 0)
223 {
224 errno = EBADF;
225 return -1;
226 }
227
228 int return_value = __VERIFIER_nondet_int();
229 __CPROVER_assume(return_value >= -1);
230 (void)dirfd;
231 (void)*pathname;
232 (void)flags;
233 return return_value;
234}
235
236/* FUNCTION: openat */
237
238int __CPROVER_openat(int dirfd, const char *pathname, int flags);
239
240 int openat(int dirfd, const char *pathname, int flags, ...)
241{
242 return __CPROVER_openat(dirfd, pathname, flags);
243}
244
245/* FUNCTION: _openat */
246
247int __CPROVER_openat(int dirfd, const char *pathname, int flags);
248
249 int _openat(int dirfd, const char *pathname, int flags, ...)
250{
251 return __CPROVER_openat(dirfd, pathname, flags);
252}
253
254/* FUNCTION: openat64 */
255
256int __CPROVER_openat(int dirfd, const char *pathname, int flags);
257
258 int openat64(int dirfd, const char *pathname, int flags, ...)
259{
260 return __CPROVER_openat(dirfd, pathname, flags);
261}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:566
void __CPROVER_assume(__CPROVER_bool assumption)
int __VERIFIER_nondet_int(void)
int open(const char *pathname, int flags,...)
Definition fcntl.c:89
int creat(const char *pathname, mode_t mode)
Definition fcntl.c:156
int _open(const char *pathname, int flags,...)
Definition fcntl.c:98
int openat(int dirfd, const char *pathname, int flags,...)
Definition fcntl.c:240
int __CPROVER_creat(const char *pathname, mode_t mode)
Definition fcntl.c:129
int _creat(const char *pathname, mode_t mode)
Definition fcntl.c:178
int openat64(int dirfd, const char *pathname, int flags,...)
Definition fcntl.c:258
int open64(const char *pathname, int flags,...)
Definition fcntl.c:107
int fcntl64(int fd, int cmd,...)
Definition fcntl.c:52
int _fcntl(int fd, int cmd,...)
Definition fcntl.c:43
#define MODE_T
Definition fcntl.c:123
int __CPROVER_open(const char *pathname, int flags)
Definition fcntl.c:75
int __CPROVER_fcntl(int fd, int cmd)
Definition fcntl.c:15
int fcntl(int fd, int cmd,...)
Definition fcntl.c:34
int _openat(int dirfd, const char *pathname, int flags,...)
Definition fcntl.c:249
int creat64(const char *pathname, mode_t mode)
Definition fcntl.c:200
int __CPROVER_openat(int dirfd, const char *pathname, int flags)
Definition fcntl.c:219
int __fcntl_time64(int fd, int cmd,...)
Definition fcntl.c:61

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