source: CIVL/examples/svcomp17/basename_false-unreach-call.c@ 1aaefd4

main test-branch
Last change on this file since 1aaefd4 was ea777aa, checked in by Alex Wilton <awilton@…>, 3 years ago

Moved examples, include, build_default.properties, common.xml, and README out from dev.civl.com into the root of the repo.

git-svn-id: ​svn://vsl.cis.udel.edu/civl/trunk@5704 fb995dde-84ed-4084-dfe6-e5aef3e2452c
  • Property mode set to 100644
File size: 10.2 KB
Line 
1extern char __VERIFIER_nondet_char(void);
2extern void __VERIFIER_assume(int);
3/*
4 This package is free software; you can redistribute it and/or modify
5 it under the terms of the GNU General Public License as published by
6 the Free Software Foundation; version 2 dated June, 1991.
7
8 This package is distributed in the hope that it will be useful,
9 but WITHOUT ANY WARRANTY; without even the implied warranty of
10 MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
11 GNU General Public License for more details.
12
13 You should have received a copy of the GNU General Public License
14 along with this package; if not, write to the Free Software
15 Foundation, Inc., 51 Franklin St, Fifth Floor, Boston,
16 MA 02110-1301, USA.
17*/
18extern void __VERIFIER_error(void);
19#include <string.h>
20#include <unistd.h>
21#include <stdlib.h>
22#define __builtin_strcmp(a,b) strcmp(a,b)
23
24#ifndef NULL
25#define NULL ((void*)0)
26#endif
27
28// file libbb/get_last_path_component.c line 25
29static char * bb_get_last_path_component_nostrip(const char *path);
30// file libbb/get_last_path_component.c line 41
31static char * bb_get_last_path_component_strip(char *path);
32// file ./libbb-dump.i line 1
33static void bb_show_usage(void);
34// file include/libbb.h line 751
35static signed long int full_write(signed int fd, const void *buf, unsigned long int len);
36// file include/libbb.h line 388
37static char * last_char_is(const char *s, signed int c);
38// file include/libbb.h line 748
39static signed long int safe_write(signed int fd, const void *buf, unsigned long int count);
40
41// file libbb/ptr_to_globals.c line 19
42static signed int * const bb_errno;
43
44// file coreutils/basename.c line 49
45signed int __main(signed int argc, char **argv)
46{
47 unsigned long int m;
48 unsigned long int n;
49 char *s;
50 if(!(argv == ((char **)NULL)))
51 (void)0;
52
53 else
54 /* assertion !(argv == ((char **)((void*)0))) */
55 __VERIFIER_error();
56 signed int tmp_statement_expression$1;
57 _Bool tmp_if_expr$2;
58 signed int tmp_if_expr$5;
59 signed int tmp_statement_expression$3;
60 signed int return_value___builtin_strcmp$4;
61 if(!(*(1l + argv) == ((char *)NULL)))
62 {
63 unsigned long int basename_main$$1$$1$$__s1_len;
64 unsigned long int __s2_len;
65 if((_Bool)1)
66 {
67 if(!((unsigned long int)("--" + 1l) + -((unsigned long int)"--") == 1ul))
68 goto __CPROVER_DUMP_L3;
69
70 __s2_len=__builtin_strlen("--");
71 tmp_if_expr$2 = (__s2_len < (unsigned long int)4 ? (signed int)(1 != 0) : (signed int)(0 != 0)) != 0;
72 }
73
74 else
75 {
76
77 __CPROVER_DUMP_L3:
78 ;
79 tmp_if_expr$2 = 0 != 0;
80 }
81 if(!(tmp_if_expr$2 == (_Bool)0))
82 {
83 const unsigned char *__s2;
84 if(!(argv == ((char **)NULL)))
85 (void)0;
86
87 else
88 /* assertion !(argv == ((char **)((void*)0))) */
89 __VERIFIER_error();
90 __s2 = (const char *)argv[(signed long int)1];
91 signed int __result;
92 if(!(__s2 == ((const unsigned char *)NULL)))
93 (void)0;
94
95 else
96 /* assertion !(__s2 == ((const unsigned char *)((void*)0))) */
97 __VERIFIER_error();
98 __result = (signed int)((const char *)"--")[(signed long int)0] - (signed int)__s2[(signed long int)0];
99 if(__s2_len > 0ul)
100 {
101 if(__result == 0)
102 {
103 if(!("--" == ((const char *)NULL)))
104 (void)0;
105
106 else
107 /* assertion !("--" == ((const unsigned char *)((void*)0))) */
108 __VERIFIER_error();
109 if(!(__s2 == ((const unsigned char *)NULL)))
110 (void)0;
111
112 else
113 /* assertion !(__s2 == ((const unsigned char *)((void*)0))) */
114 __VERIFIER_error();
115 __result = (signed int)((const char *)"--")[(signed long int)1] - (signed int)__s2[(signed long int)1];
116 if(__s2_len > 1ul)
117 {
118 if(__result == 0)
119 {
120 if(!("--" == ((const char *)NULL)))
121 (void)0;
122
123 else
124 /* assertion !("--" == ((const unsigned char *)((void*)0))) */
125 __VERIFIER_error();
126 if(!(__s2 == ((const unsigned char *)NULL)))
127 (void)0;
128
129 else
130 /* assertion !(__s2 == ((const unsigned char *)((void*)0))) */
131 __VERIFIER_error();
132 __result = (signed int)((const char *)"--")[(signed long int)2] - (signed int)__s2[(signed long int)2];
133 if(__s2_len > 2ul)
134 {
135 if(__result == 0)
136 {
137 if(!("--" == ((const char *)NULL)))
138 (void)0;
139
140 else
141 /* assertion !("--" == ((const unsigned char *)((void*)0))) */
142 __VERIFIER_error();
143 /* assertion (_Bool)0 */
144 __VERIFIER_error();
145 if(!(__s2 == ((const unsigned char *)NULL)))
146 (void)0;
147
148 else
149 /* assertion !(__s2 == ((const unsigned char *)((void*)0))) */
150 __VERIFIER_error();
151 __result = (signed int)((const char *)"--")[(signed long int)3] - (signed int)__s2[(signed long int)3];
152 }
153
154 }
155
156 }
157
158 }
159
160 }
161
162 }
163
164 tmp_statement_expression$3 = __result;
165 tmp_if_expr$5 = -tmp_statement_expression$3;
166 }
167
168 else
169 {
170 if(!(argv == ((char **)NULL)))
171 (void)0;
172
173 else
174 /* assertion !(argv == ((char **)((void*)0))) */
175 __VERIFIER_error();
176 return_value___builtin_strcmp$4=__builtin_strcmp(argv[(signed long int)1], "--");
177 tmp_if_expr$5 = return_value___builtin_strcmp$4;
178 }
179 tmp_statement_expression$1 = tmp_if_expr$5;
180 if(tmp_statement_expression$1 == 0)
181 {
182 argv = argv + 1l;
183 argc = argc - 1;
184 }
185
186 }
187
188 if(4294967294u + (unsigned int)argc >= 2u)
189 bb_show_usage();
190
191 argv = argv + 1l;
192 if(!(argv == ((char **)NULL)))
193 (void)0;
194
195 else
196 /* assertion !(argv == ((char **)((void*)0))) */
197 __VERIFIER_error();
198 s=bb_get_last_path_component_strip(*argv);
199 m=strlen(s);
200 argv = argv + 1l;
201 if(!(argv == ((char **)NULL)))
202 (void)0;
203
204 else
205 /* assertion !(argv == ((char **)((void*)0))) */
206 __VERIFIER_error();
207 signed int tmp_statement_expression$6;
208 if(!(*argv == ((char *)NULL)))
209 {
210 n=strlen(*argv);
211 if(!(n >= m))
212 {
213 unsigned long int __s1_len;
214 unsigned long int basename_main$$1$$4$$1$$__s2_len;
215 signed int return_value___builtin_strcmp$7;
216 if(!(argv == ((char **)NULL)))
217 (void)0;
218
219 else
220 /* assertion !(argv == ((char **)((void*)0))) */
221 __VERIFIER_error();
222 return_value___builtin_strcmp$7=__builtin_strcmp((s + (signed long int)m) - (signed long int)n, *argv);
223 tmp_statement_expression$6 = return_value___builtin_strcmp$7;
224 if(tmp_statement_expression$6 == 0)
225 m = m - n;
226
227 }
228
229 }
230
231 unsigned long int tmp_post$8 = m;
232 m = m + 1ul;
233 if(!(s == ((char *)NULL)))
234 (void)0;
235
236 else
237 /* assertion !(s == ((char *)((void*)0))) */
238 __VERIFIER_error();
239 s[(signed long int)tmp_post$8] = (char)10;
240 signed long int return_value_full_write$9;
241 return_value_full_write$9=full_write(1, (const void *)s, m);
242 return (signed int)(return_value_full_write$9 != (signed long int)m);
243}
244
245// file libbb/get_last_path_component.c line 25
246static char * bb_get_last_path_component_nostrip(const char *path)
247{
248 char *slash;
249 slash=strrchr(path, 47);
250 _Bool tmp_if_expr$2;
251 _Bool tmp_if_expr$1;
252 if(slash == ((char *)NULL))
253 tmp_if_expr$2 = 1 != 0;
254
255 else
256 {
257 if(slash == path)
258 tmp_if_expr$1 = (!((signed int)slash[(signed long int)1] != 0) ? (signed int)(1 != 0) : (signed int)(0 != 0)) != 0;
259
260 else
261 tmp_if_expr$1 = 0 != 0;
262 tmp_if_expr$2 = (tmp_if_expr$1 != (_Bool)0 ? (signed int)(1 != 0) : (signed int)(0 != 0)) != 0;
263 }
264 if(!(tmp_if_expr$2 == (_Bool)0))
265 return (char *)path;
266
267 return slash + (signed long int)1;
268}
269
270// file libbb/get_last_path_component.c line 41
271static char * bb_get_last_path_component_strip(char *path)
272{
273 char *slash;
274 slash=last_char_is(path, 47);
275 char *tmp_post$1;
276 if(!(slash == ((char *)NULL)))
277 for( ; (signed int)*slash == 47; *tmp_post$1 = (char)0)
278 {
279 if(slash == path)
280 break;
281
282 tmp_post$1 = slash;
283 slash = slash - 1l;
284 }
285
286 char *return_value_bb_get_last_path_component_nostrip$2;
287 return_value_bb_get_last_path_component_nostrip$2=bb_get_last_path_component_nostrip(path);
288 return return_value_bb_get_last_path_component_nostrip$2;
289}
290
291// file ./libbb-dump.i line 1
292static void bb_show_usage(void)
293{
294 ;
295}
296
297// file include/libbb.h line 751
298static signed long int full_write(signed int fd, const void *buf, unsigned long int len)
299{
300 signed long int cc;
301 signed long int total = (signed long int)0;
302 for( ; !(len == 0ul); len = len - (unsigned long int)cc)
303 {
304 cc=safe_write(fd, buf, len);
305 if(cc < 0l)
306 {
307 if(!(total == 0l))
308 return total;
309
310 return cc;
311 }
312
313 total = total + cc;
314 buf = (const void *)((const char *)buf + cc);
315 }
316 return total;
317}
318
319// file include/libbb.h line 388
320static char * last_char_is(const char *s, signed int c)
321{
322 if(!(s == ((const char *)NULL)))
323 {
324 if(!((signed int)*s == 0))
325 {
326 unsigned long int sz;
327 unsigned long int return_value_strlen$1;
328 return_value_strlen$1=strlen(s);
329 sz = return_value_strlen$1 - (unsigned long int)1;
330 s = s + (signed long int)sz;
331 if((signed int)*s == c)
332 return (char *)s;
333
334 }
335
336 }
337
338 return (char *)NULL;
339}
340
341// file include/libbb.h line 748
342static signed long int safe_write(signed int fd, const void *buf, unsigned long int count)
343{
344 signed long int n;
345 _Bool tmp_if_expr$1;
346 do
347 {
348 n=count; //write(fd, buf, count);
349 if(n < 0l)
350 tmp_if_expr$1 = (*bb_errno == 4 ? (signed int)(1 != 0) : (signed int)(0 != 0)) != 0;
351
352 else
353 tmp_if_expr$1 = 0 != 0;
354 }
355 while(tmp_if_expr$1 != (_Bool)0);
356 return n;
357}
358
359
360int main()
361{
362 int argc = __VERIFIER_nondet_int();
363 __VERIFIER_assume(argc>=0);
364
365 char **argv=malloc((argc+1)*sizeof(char*));
366 argv[argc]=0;
367
368 for(int i=0; i<argc; ++i)
369 {
370 // let's limit the size of arguments to 10, which is an
371 // underapproximation obviously
372 argv[i]=malloc(10);
373 for(int j=0; j<10; ++j)
374 argv[i][j]=__VERIFIER_nondet_char();
375 }
376
377 return __main(argc, argv);
378}
Note: See TracBrowser for help on using the repository browser.