CBMC
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 
14 
15 int __CPROVER_fcntl(int fd, int cmd)
16 {
17 __CPROVER_HIDE:;
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 
32 int __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 
41 int __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 
50 int __CPROVER_fcntl(int, int);
51 
52 int fcntl64(int fd, int cmd, ...)
53 {
54  return __CPROVER_fcntl(fd, cmd);
55 }
56 
57 /* FUNCTION: __CPROVER_open */
58 
59 #ifndef __CPROVER_FCNTL_H_INCLUDED
60 # include <fcntl.h>
61 # define __CPROVER_FCNTL_H_INCLUDED
62 #endif
63 
64 int __VERIFIER_nondet_int(void);
65 
66 int __CPROVER_open(const char *pathname, int flags)
67 {
68 __CPROVER_HIDE:;
69  int return_value = __VERIFIER_nondet_int();
70  __CPROVER_assume(return_value >= -1);
71  (void)*pathname;
72  (void)flags;
73  return return_value;
74 }
75 
76 /* FUNCTION: open */
77 
78 int __CPROVER_open(const char *, int);
79 
80 int open(const char *pathname, int flags, ...)
81 {
82  return __CPROVER_open(pathname, flags);
83 }
84 
85 /* FUNCTION: _open */
86 
87 int __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: open64 */
95 
96 int __CPROVER_open(const char *, int);
97 
98 int open64(const char *pathname, int flags, ...)
99 {
100  return __CPROVER_open(pathname, flags);
101 }
102 
103 /* FUNCTION: __CPROVER_creat */
104 
105 #ifndef __CPROVER_FCNTL_H_INCLUDED
106 # include <fcntl.h>
107 # define __CPROVER_FCNTL_H_INCLUDED
108 #endif
109 
110 #ifndef MODE_T
111 # ifdef _WIN32
112 # define MODE_T int
113 # else
114 # define MODE_T mode_t
115 # endif
116 #endif
117 
118 int __VERIFIER_nondet_int(void);
119 
120 int __CPROVER_creat(const char *pathname, MODE_T mode)
121 {
122 __CPROVER_HIDE:;
123  int return_value = __VERIFIER_nondet_int();
124  __CPROVER_assume(return_value >= -1);
125  (void)*pathname;
126  (void)mode;
127  return return_value;
128 }
129 
130 /* FUNCTION: creat */
131 
132 #ifndef __CPROVER_FCNTL_H_INCLUDED
133 # include <fcntl.h>
134 # define __CPROVER_FCNTL_H_INCLUDED
135 #endif
136 
137 #ifndef MODE_T
138 # ifdef _WIN32
139 # define MODE_T int
140 # else
141 # define MODE_T mode_t
142 # endif
143 #endif
144 
145 int __CPROVER_creat(const char *, MODE_T);
146 
147 int creat(const char *pathname, MODE_T mode)
148 {
149  return __CPROVER_creat(pathname, mode);
150 }
151 
152 /* FUNCTION: _creat */
153 
154 #ifndef __CPROVER_FCNTL_H_INCLUDED
155 # include <fcntl.h>
156 # define __CPROVER_FCNTL_H_INCLUDED
157 #endif
158 
159 #ifndef MODE_T
160 # ifdef _WIN32
161 # define MODE_T int
162 # else
163 # define MODE_T mode_t
164 # endif
165 #endif
166 
167 int __CPROVER_creat(const char *, MODE_T);
168 
169 int _creat(const char *pathname, MODE_T mode)
170 {
171  return __CPROVER_creat(pathname, mode);
172 }
173 
174 /* FUNCTION: creat64 */
175 
176 #ifndef __CPROVER_FCNTL_H_INCLUDED
177 # include <fcntl.h>
178 # define __CPROVER_FCNTL_H_INCLUDED
179 #endif
180 
181 #ifndef MODE_T
182 # ifdef _WIN32
183 # define MODE_T int
184 # else
185 # define MODE_T mode_t
186 # endif
187 #endif
188 
189 int __CPROVER_creat(const char *, MODE_T);
190 
191 int creat64(const char *pathname, MODE_T mode)
192 {
193  return __CPROVER_creat(pathname, mode);
194 }
195 
196 /* FUNCTION: __CPROVER_openat */
197 
198 #ifndef __CPROVER_FCNTL_H_INCLUDED
199 # include <fcntl.h>
200 # define __CPROVER_FCNTL_H_INCLUDED
201 #endif
202 
203 #ifndef __CPROVER_ERRNO_H_INCLUDED
204 # include <errno.h>
205 # define __CPROVER_ERRNO_H_INCLUDED
206 #endif
207 
208 int __VERIFIER_nondet_int(void);
209 
210 int __CPROVER_openat(int dirfd, const char *pathname, int flags)
211 {
212 __CPROVER_HIDE:;
213  if(dirfd < 0)
214  {
215  errno = EBADF;
216  return -1;
217  }
218 
219  int return_value = __VERIFIER_nondet_int();
220  __CPROVER_assume(return_value >= -1);
221  (void)dirfd;
222  (void)*pathname;
223  (void)flags;
224  return return_value;
225 }
226 
227 /* FUNCTION: openat */
228 
229 int __CPROVER_openat(int dirfd, const char *pathname, int flags);
230 
231 int openat(int dirfd, const char *pathname, int flags, ...)
232 {
233  return __CPROVER_openat(dirfd, pathname, flags);
234 }
235 
236 /* FUNCTION: _openat */
237 
238 int __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: openat64 */
246 
247 int __CPROVER_openat(int dirfd, const char *pathname, int flags);
248 
249 int openat64(int dirfd, const char *pathname, int flags, ...)
250 {
251  return __CPROVER_openat(dirfd, pathname, flags);
252 }
void __CPROVER_assume(__CPROVER_bool assumption)
int __VERIFIER_nondet_int(void)
int open(const char *pathname, int flags,...)
Definition: fcntl.c:80
int creat(const char *pathname, mode_t mode)
Definition: fcntl.c:147
int _open(const char *pathname, int flags,...)
Definition: fcntl.c:89
int openat(int dirfd, const char *pathname, int flags,...)
Definition: fcntl.c:231
int __CPROVER_creat(const char *pathname, mode_t mode)
Definition: fcntl.c:120
int _creat(const char *pathname, mode_t mode)
Definition: fcntl.c:169
int openat64(int dirfd, const char *pathname, int flags,...)
Definition: fcntl.c:249
int open64(const char *pathname, int flags,...)
Definition: fcntl.c:98
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:114
int __CPROVER_open(const char *pathname, int flags)
Definition: fcntl.c:66
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:240
int creat64(const char *pathname, mode_t mode)
Definition: fcntl.c:191
int __CPROVER_openat(int dirfd, const char *pathname, int flags)
Definition: fcntl.c:210