1void __VERIFIER_assert(int cond) {
2 if (!(cond)) {
3 ERROR: goto ERROR;
4 }
5 return;
6}
7
8typedef long unsigned int size_t;
9
10extern void *memcpy (void *__restrict __dest,
11 __const void *__restrict __src, size_t __n)
12 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
13extern void *memmove (void *__dest, __const void *__src, size_t __n)
14 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
15
16extern void *memccpy (void *__restrict __dest, __const void *__restrict __src,
17 int __c, size_t __n)
18 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
19
20extern void *memset (void *__s, int __c, size_t __n) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
21extern int memcmp (__const void *__s1, __const void *__s2, size_t __n)
22 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__pure__)) __attribute__ ((__nonnull__ (1, 2)));
23extern void *memchr (__const void *__s, int __c, size_t __n)
24 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__pure__)) __attribute__ ((__nonnull__ (1)));
25
26
27extern char *strcpy (char *__restrict __dest, __const char *__restrict __src)
28 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
29extern char *strncpy (char *__restrict __dest,
30 __const char *__restrict __src, size_t __n)
31 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
32extern char *strcat (char *__restrict __dest, __const char *__restrict __src)
33 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
34extern char *strncat (char *__restrict __dest, __const char *__restrict __src,
35 size_t __n) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
36extern int strcmp (__const char *__s1, __const char *__s2)
37 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__pure__)) __attribute__ ((__nonnull__ (1, 2)));
38extern int strncmp (__const char *__s1, __const char *__s2, size_t __n)
39 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__pure__)) __attribute__ ((__nonnull__ (1, 2)));
40extern int strcoll (__const char *__s1, __const char *__s2)
41 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__pure__)) __attribute__ ((__nonnull__ (1, 2)));
42extern size_t strxfrm (char *__restrict __dest,
43 __const char *__restrict __src, size_t __n)
44 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (2)));
45
46typedef struct __locale_struct
47{
48 struct __locale_data *__locales[13];
49 const unsigned short int *__ctype_b;
50 const int *__ctype_tolower;
51 const int *__ctype_toupper;
52 const char *__names[13];
53} *__locale_t;
54typedef __locale_t locale_t;
55extern int strcoll_l (__const char *__s1, __const char *__s2, __locale_t __l)
56 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__pure__)) __attribute__ ((__nonnull__ (1, 2, 3)));
57extern size_t strxfrm_l (char *__dest, __const char *__src, size_t __n,
58 __locale_t __l) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (2, 4)));
59extern char *strdup (__const char *__s)
60 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__malloc__)) __attribute__ ((__nonnull__ (1)));
61extern char *strndup (__const char *__string, size_t __n)
62 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__malloc__)) __attribute__ ((__nonnull__ (1)));
63
64extern char *strchr (__const char *__s, int __c)
65 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__pure__)) __attribute__ ((__nonnull__ (1)));
66extern char *strrchr (__const char *__s, int __c)
67 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__pure__)) __attribute__ ((__nonnull__ (1)));
68
69
70extern size_t strcspn (__const char *__s, __const char *__reject)
71 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__pure__)) __attribute__ ((__nonnull__ (1, 2)));
72extern size_t strspn (__const char *__s, __const char *__accept)
73 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__pure__)) __attribute__ ((__nonnull__ (1, 2)));
74extern char *strpbrk (__const char *__s, __const char *__accept)
75 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__pure__)) __attribute__ ((__nonnull__ (1, 2)));
76extern char *strstr (__const char *__haystack, __const char *__needle)
77 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__pure__)) __attribute__ ((__nonnull__ (1, 2)));
78extern char *strtok (char *__restrict __s, __const char *__restrict __delim)
79 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (2)));
80
81extern char *__strtok_r (char *__restrict __s,
82 __const char *__restrict __delim,
83 char **__restrict __save_ptr)
84 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (2, 3)));
85extern char *strtok_r (char *__restrict __s, __const char *__restrict __delim,
86 char **__restrict __save_ptr)
87 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (2, 3)));
88
89extern size_t strlen (__const char *__s)
90 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__pure__)) __attribute__ ((__nonnull__ (1)));
91
92extern size_t strnlen (__const char *__string, size_t __maxlen)
93 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__pure__)) __attribute__ ((__nonnull__ (1)));
94
95extern char *strerror (int __errnum) __attribute__ ((__nothrow__ , __leaf__));
96
97extern int strerror_r (int __errnum, char *__buf, size_t __buflen) __asm__ ("" "__xpg_strerror_r") __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (2)));
98extern char *strerror_l (int __errnum, __locale_t __l) __attribute__ ((__nothrow__ , __leaf__));
99extern void __bzero (void *__s, size_t __n) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
100extern void bcopy (__const void *__src, void *__dest, size_t __n)
101 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
102extern void bzero (void *__s, size_t __n) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
103extern int bcmp (__const void *__s1, __const void *__s2, size_t __n)
104 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__pure__)) __attribute__ ((__nonnull__ (1, 2)));
105extern char *index (__const char *__s, int __c)
106 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__pure__)) __attribute__ ((__nonnull__ (1)));
107extern char *rindex (__const char *__s, int __c)
108 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__pure__)) __attribute__ ((__nonnull__ (1)));
109extern int ffs (int __i) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__));
110extern int strcasecmp (__const char *__s1, __const char *__s2)
111 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__pure__)) __attribute__ ((__nonnull__ (1, 2)));
112extern int strncasecmp (__const char *__s1, __const char *__s2, size_t __n)
113 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__pure__)) __attribute__ ((__nonnull__ (1, 2)));
114extern char *strsep (char **__restrict __stringp,
115 __const char *__restrict __delim)
116 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
117extern char *strsignal (int __sig) __attribute__ ((__nothrow__ , __leaf__));
118extern char *__stpcpy (char *__restrict __dest, __const char *__restrict __src)
119 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
120extern char *stpcpy (char *__restrict __dest, __const char *__restrict __src)
121 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
122extern char *__stpncpy (char *__restrict __dest,
123 __const char *__restrict __src, size_t __n)
124 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
125extern char *stpncpy (char *__restrict __dest,
126 __const char *__restrict __src, size_t __n)
127 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
128
129extern int __VERIFIER_nondet_int(void);
130int bar(char *x)
131{
132 return __VERIFIER_nondet_int();
133}
134int foo(int * x){
135 *x = __VERIFIER_nondet_int();
136 return *x;
137}
138int main(){
139 int i,j,ret,offset, tmp_cnt, tel_data,klen;
140 char x [1000];
141 for (i = 0; i < 1000; ++i)
142 x[i]= __VERIFIER_nondet_int();
143 for (i= 0; i < 1000; ++i){
144 ret = __VERIFIER_nondet_int();
145 if (ret != 0)
146 return -1;
147 tmp_cnt = __VERIFIER_nondet_int();
148 if (tmp_cnt < 0)
149 return -1;
150 for ( offset = 0; offset < tmp_cnt; offset++ )
151 {
152 ret = foo(&tel_data ) ;
153 if ( ( ret == 0 ) || ( ret == 1 ) )
154 {
155 return 1 ;
156 }
157 else if ( ret == -1 )
158 {
159 continue ;
160 }
161 for ( j = 0; x[j] != 0; j++ )
162 {
163 if ( x[i] == 1)
164 {
165 memmove( &x[i], &x[i + 1], (1001) - ( i + 1 ) ) ;
166 }
167 }
168 ret = bar( x) ;
169 if ( ret != -1 )
170 {
171 continue ;
172 }
173 klen = strlen(x ) ;
174 if ( klen > 20 )
175 {
176 x[i]=0;
177 }
178 else if ( klen > 0 )
179 {
180 x[i] = -1;
181 }
182 }
183 }
184 __VERIFIER_assert(offset>=0 && offset<=1000);
185 return 1;
186}