CBMC
string.c
Go to the documentation of this file.
1 /* FUNCTION: __builtin___strcpy_chk */
2 
3 char *__builtin___strcpy_chk(char *dst, const char *src, __CPROVER_size_t s)
4 {
5 __CPROVER_HIDE:;
6 
7 #ifdef __CPROVER_STRING_ABSTRACTION
8  __CPROVER_precondition(
9  __CPROVER_is_zero_string(src), "strcpy zero-termination of 2nd argument");
10  __CPROVER_precondition(
11  __CPROVER_buffer_size(dst) > __CPROVER_zero_string_length(src),
12  "strcpy buffer overflow");
13  __CPROVER_precondition(
14  s == ~(__CPROVER_size_t)0 || __CPROVER_buffer_size(dst) == s,
15  "builtin object size");
16  dst[__CPROVER_zero_string_length(src)] = 0;
17  __CPROVER_is_zero_string(dst) = 1;
18  __CPROVER_zero_string_length(dst) = __CPROVER_zero_string_length(src);
19 #else
20  __CPROVER_precondition(
21  __CPROVER_POINTER_OBJECT(dst) != __CPROVER_POINTER_OBJECT(src),
22  "strcpy src/dst overlap");
23  __CPROVER_size_t i = 0;
24  char ch;
25  do
26  {
27  ch = src[i];
28  dst[i] = ch;
29  i++;
30  } while(i < s && ch != (char)0);
31 #endif
32  return dst;
33 }
34 
35 /* FUNCTION: __builtin___strcat_chk */
36 
37 __inline char *__builtin___strcat_chk(char *dst, const char *src, __CPROVER_size_t s)
38 {
39 __CPROVER_HIDE:;
40 
41 #ifdef __CPROVER_STRING_ABSTRACTION
42  __CPROVER_size_t new_size;
43  __CPROVER_precondition(
44  __CPROVER_is_zero_string(dst), "strcat zero-termination of 1st argument");
45  __CPROVER_precondition(
46  __CPROVER_is_zero_string(src), "strcat zero-termination of 2nd argument");
47  __CPROVER_precondition(
48  s == ~(__CPROVER_size_t)0 || __CPROVER_buffer_size(dst) == s,
49  "builtin object size");
50  new_size =
51  __CPROVER_zero_string_length(dst) + __CPROVER_zero_string_length(src);
52  __CPROVER_assert(
53  __CPROVER_buffer_size(dst) > new_size, "strcat buffer overflow");
54  __CPROVER_size_t old_size = __CPROVER_zero_string_length(dst);
55  //" for(size_t i=0; i<__CPROVER_zero_string_length(src); i++)
56  //" dst[old_size+i];
57  dst[new_size] = 0;
58  __CPROVER_is_zero_string(dst) = 1;
59  __CPROVER_zero_string_length(dst) = new_size;
60 #else
61  __CPROVER_precondition(
62  __CPROVER_POINTER_OBJECT(dst) != __CPROVER_POINTER_OBJECT(src),
63  "strcat src/dst overlap");
64  __CPROVER_size_t i = 0;
65  while(dst[i] != 0)
66  i++;
67 
68  __CPROVER_size_t j = 0;
69  char ch = 1;
70  for(; i < s && ch != (char)0; ++i, ++j)
71  {
72  ch = src[j];
73  dst[i] = ch;
74  }
75 #endif
76  return dst;
77 }
78 
79 /* FUNCTION: __builtin___strncat_chk */
80 
81 __inline char *__builtin___strncat_chk(
82  char *dst, const char *src, __CPROVER_size_t n, __CPROVER_size_t s)
83 {
84 __CPROVER_HIDE:;
85 #ifdef __CPROVER_STRING_ABSTRACTION
86  __CPROVER_size_t additional, new_size;
87  __CPROVER_precondition(
88  __CPROVER_is_zero_string(dst), "strncat zero-termination of 1st argument");
89  __CPROVER_precondition(
90  __CPROVER_is_zero_string(src) || __CPROVER_buffer_size(src) >= n,
91  "strncat zero-termination of 2nd argument");
92  __CPROVER_precondition(
93  s == ~(__CPROVER_size_t)0 || __CPROVER_buffer_size(dst) == s,
94  "builtin object size");
95  additional = (n < __CPROVER_zero_string_length(src))
96  ? n
97  : __CPROVER_zero_string_length(src);
98  new_size = __CPROVER_is_zero_string(dst) + additional;
99  __CPROVER_assert(
100  __CPROVER_buffer_size(dst) > new_size, "strncat buffer overflow");
101  __CPROVER_size_t dest_len = __CPROVER_zero_string_length(dst);
102  __CPROVER_size_t i;
103  for(i = 0; i < n && i < __CPROVER_zero_string_length(src); i++)
104  dst[dest_len + i] = src[i];
105  dst[dest_len + i] = 0;
106  __CPROVER_is_zero_string(dst) = 1;
107  __CPROVER_zero_string_length(dst) = new_size;
108 #else
109  __CPROVER_precondition(
110  __CPROVER_POINTER_OBJECT(dst) != __CPROVER_POINTER_OBJECT(src),
111  "strncat src/dst overlap");
112 
113  __CPROVER_size_t i = 0;
114  while(dst[i] != 0)
115  i++;
116 
117  __CPROVER_size_t j = 0;
118  char ch = 1;
119  for(; i < s && j < n && ch != (char)0; ++i, ++j)
120  {
121  ch = src[j];
122  dst[i] = ch;
123  }
124  if(ch != (char)0)
125  dst[i] = '\0';
126 #endif
127  return dst;
128 }
129 
130 /* FUNCTION: strcpy */
131 
132 #ifndef __CPROVER_STRING_H_INCLUDED
133 #include <string.h>
134 #define __CPROVER_STRING_H_INCLUDED
135 #endif
136 
137 #undef strcpy
138 
139 char *strcpy(char *dst, const char *src)
140 {
141 __CPROVER_HIDE:;
142 #ifdef __CPROVER_STRING_ABSTRACTION
143  __CPROVER_precondition(
144  __CPROVER_is_zero_string(src), "strcpy zero-termination of 2nd argument");
145  __CPROVER_precondition(
146  __CPROVER_buffer_size(dst) > __CPROVER_zero_string_length(src),
147  "strcpy buffer overflow");
148  dst[__CPROVER_zero_string_length(src)] = 0;
149  __CPROVER_is_zero_string(dst) = 1;
150  __CPROVER_zero_string_length(dst) = __CPROVER_zero_string_length(src);
151 #else
152  __CPROVER_precondition(
153  __CPROVER_POINTER_OBJECT(dst) != __CPROVER_POINTER_OBJECT(src),
154  "strcpy src/dst overlap");
155  __CPROVER_size_t i = 0;
156  char ch;
157  do
158  {
159  ch = src[i];
160  dst[i] = ch;
161  i++;
162  } while(ch != (char)0);
163 #endif
164  return dst;
165 }
166 
167 /* FUNCTION: strncpy */
168 
169 #ifndef __CPROVER_STRING_H_INCLUDED
170 #include <string.h>
171 #define __CPROVER_STRING_H_INCLUDED
172 #endif
173 
174 #undef strncpy
175 
176 char *strncpy(char *dst, const char *src, size_t n)
177 {
178 __CPROVER_HIDE:;
179 #ifdef __CPROVER_STRING_ABSTRACTION
180  __CPROVER_precondition(
181  __CPROVER_is_zero_string(src), "strncpy zero-termination of 2nd argument");
182  __CPROVER_precondition(
183  __CPROVER_buffer_size(dst) >= n, "strncpy buffer overflow");
184  __CPROVER_is_zero_string(dst) = __CPROVER_zero_string_length(src) < n;
185  __CPROVER_zero_string_length(dst) = __CPROVER_zero_string_length(src);
186 #else
187  __CPROVER_precondition(
188  __CPROVER_POINTER_OBJECT(dst) != __CPROVER_POINTER_OBJECT(src) ||
189  (src >= dst + n) || (dst >= src + n),
190  "strncpy src/dst overlap");
191  __CPROVER_size_t i = 0;
192  char ch;
193  _Bool end;
194 
195  // We use a single loop to make bounds checking etc easier.
196  // Note that strncpy _always_ writes 'n' characters into 'dst'.
197  for(end = 0; i < n; i++)
198  {
199  ch = end ? 0 : src[i];
200  dst[i] = ch;
201  end = end || ch == (char)0;
202  }
203 #endif
204  return dst;
205 }
206 
207 /* FUNCTION: __builtin___strncpy_chk */
208 
209 #ifndef __CPROVER_STRING_H_INCLUDED
210 #include <string.h>
211 #define __CPROVER_STRING_H_INCLUDED
212 #endif
213 
214 char *__builtin___strncpy_chk(
215  char *dst,
216  const char *src,
217  size_t n,
218  size_t object_size)
219 {
220 __CPROVER_HIDE:;
221 #ifdef __CPROVER_STRING_ABSTRACTION
222  __CPROVER_precondition(
223  __CPROVER_is_zero_string(src), "strncpy zero-termination of 2nd argument");
224  __CPROVER_precondition(
225  __CPROVER_buffer_size(dst) >= n, "strncpy buffer overflow");
226  __CPROVER_precondition(
227  object_size == ~(size_t)0 || __CPROVER_buffer_size(dst) == object_size,
228  "strncpy object size");
229  __CPROVER_is_zero_string(dst) = __CPROVER_zero_string_length(src) < n;
230  __CPROVER_zero_string_length(dst) = __CPROVER_zero_string_length(src);
231 #else
232  __CPROVER_precondition(
233  __CPROVER_POINTER_OBJECT(dst) != __CPROVER_POINTER_OBJECT(src) ||
234  (src >= dst + n) || (dst >= src + n),
235  "strncpy src/dst overlap");
236  __CPROVER_size_t i = 0;
237  char ch;
238  _Bool end;
239  (void)object_size;
240 
241  // We use a single loop to make bounds checking etc easier.
242  // Note that strncpy _always_ writes 'n' characters into 'dst'.
243  for(end = 0; i < n; i++)
244  {
245  ch = end ? 0 : src[i];
246  dst[i] = ch;
247  end = end || ch == (char)0;
248  }
249 #endif
250  return dst;
251 }
252 
253 /* FUNCTION: strcat */
254 
255 #ifndef __CPROVER_STRING_H_INCLUDED
256 #include <string.h>
257 #define __CPROVER_STRING_H_INCLUDED
258 #endif
259 
260 #undef strcat
261 
262 char *strcat(char *dst, const char *src)
263 {
264 __CPROVER_HIDE:;
265 #ifdef __CPROVER_STRING_ABSTRACTION
266  __CPROVER_size_t new_size;
267  __CPROVER_precondition(__CPROVER_is_zero_string(dst),
268  "strcat zero-termination of 1st argument");
269  __CPROVER_precondition(__CPROVER_is_zero_string(src),
270  "strcat zero-termination of 2nd argument");
271  new_size=__CPROVER_zero_string_length(dst)+__CPROVER_zero_string_length(src);
272  __CPROVER_assert(__CPROVER_buffer_size(dst)>new_size,
273  "strcat buffer overflow");
274  __CPROVER_size_t old_size=__CPROVER_zero_string_length(dst);
275  //" for(size_t i=0; i<__CPROVER_zero_string_length(src); i++)
276  //" dst[old_size+i];
277  dst[new_size]=0;
278  __CPROVER_is_zero_string(dst)=1;
279  __CPROVER_zero_string_length(dst)=new_size;
280 #else
281  __CPROVER_precondition(
282  __CPROVER_POINTER_OBJECT(dst) != __CPROVER_POINTER_OBJECT(src),
283  "strcat src/dst overlap");
284  __CPROVER_size_t i = 0;
285  while(dst[i] != 0)
286  i++;
287 
288  __CPROVER_size_t j = 0;
289  char ch = 1;
290  for(; ch != (char)0; ++i, ++j)
291  {
292  ch = src[j];
293  dst[i] = ch;
294  }
295 #endif
296  return dst;
297 }
298 
299 /* FUNCTION: strncat */
300 
301 #ifndef __CPROVER_STRING_H_INCLUDED
302 #include <string.h>
303 #define __CPROVER_STRING_H_INCLUDED
304 #endif
305 
306 #undef strncat
307 
308 char *strncat(char *dst, const char *src, size_t n)
309 {
310 __CPROVER_HIDE:;
311 #ifdef __CPROVER_STRING_ABSTRACTION
312  __CPROVER_size_t additional, new_size;
313  __CPROVER_precondition(
314  __CPROVER_is_zero_string(dst), "strncat zero-termination of 1st argument");
315  __CPROVER_precondition(
316  __CPROVER_is_zero_string(src) || __CPROVER_buffer_size(src) >= n,
317  "strncat zero-termination of 2nd argument");
318  additional = (n < __CPROVER_zero_string_length(src))
319  ? n
320  : __CPROVER_zero_string_length(src);
321  new_size = __CPROVER_is_zero_string(dst) + additional;
322  __CPROVER_assert(
323  __CPROVER_buffer_size(dst) > new_size, "strncat buffer overflow");
324  __CPROVER_size_t dest_len = __CPROVER_zero_string_length(dst);
325  __CPROVER_size_t i;
326  for(i = 0; i < n && i < __CPROVER_zero_string_length(src); i++)
327  dst[dest_len + i] = src[i];
328  dst[dest_len + i] = 0;
329  __CPROVER_is_zero_string(dst) = 1;
330  __CPROVER_zero_string_length(dst) = new_size;
331 #else
332  __CPROVER_precondition(
333  __CPROVER_POINTER_OBJECT(dst) != __CPROVER_POINTER_OBJECT(src) ||
334  (src >= dst + n) || (dst >= src + n),
335  "strncat src/dst overlap");
336 
337  __CPROVER_size_t i = 0;
338  while(dst[i] != 0)
339  i++;
340 
341  __CPROVER_size_t j = 0;
342  char ch = 1;
343  for(; j < n && ch != (char)0; ++i, ++j)
344  {
345  ch = src[j];
346  dst[i] = ch;
347  }
348  if(ch != (char)0)
349  dst[i] = '\0';
350 #endif
351  return dst;
352 }
353 
354 /* FUNCTION: strcmp */
355 
356 #ifndef __CPROVER_STRING_H_INCLUDED
357 #include <string.h>
358 #define __CPROVER_STRING_H_INCLUDED
359 #endif
360 
361 #undef strcmp
362 
363 int strcmp(const char *s1, const char *s2)
364 {
365 __CPROVER_HIDE:;
366 #ifdef __CPROVER_STRING_ABSTRACTION
367  int retval;
368  __CPROVER_precondition(__CPROVER_is_zero_string(s1),
369  "strcmp zero-termination of 1st argument");
370  __CPROVER_precondition(__CPROVER_is_zero_string(s2),
371  "strcmp zero-termination of 2nd argument");
372 
373  if(__CPROVER_zero_string_length(s1) != __CPROVER_zero_string_length(s2))
374  __CPROVER_assume(retval!=0);
375 
376  return retval;
377 #else
378  __CPROVER_size_t i=0;
379  unsigned char ch1, ch2;
380  do
381  {
382 # pragma CPROVER check push
383 # pragma CPROVER check disable "conversion"
384  ch1=s1[i];
385  ch2=s2[i];
386 # pragma CPROVER check pop
387 
388  if(ch1==ch2)
389  {
390  }
391  else if(ch1<ch2)
392  return -1;
393  else
394  return 1;
395 
396  i++;
397  }
398  while(ch1!=0 && ch2!=0);
399  return 0;
400 #endif
401 }
402 
403 /* FUNCTION: strcasecmp */
404 
405 #ifndef __CPROVER_STRING_H_INCLUDED
406 #include <string.h>
407 #define __CPROVER_STRING_H_INCLUDED
408 #endif
409 
410 #undef strcasecmp
411 
412 int strcasecmp(const char *s1, const char *s2)
413 {
414 __CPROVER_HIDE:;
415 #ifdef __CPROVER_STRING_ABSTRACTION
416  int retval;
417  __CPROVER_precondition(__CPROVER_is_zero_string(s1),
418  "strcasecmp zero-termination of 1st argument");
419  __CPROVER_precondition(__CPROVER_is_zero_string(s2),
420  "strcasecmp zero-termination of 2nd argument");
421 
422  if(__CPROVER_zero_string_length(s1) != __CPROVER_zero_string_length(s2))
423  __CPROVER_assume(retval!=0);
424 
425  return retval;
426 #else
427  __CPROVER_size_t i=0;
428  unsigned char ch1, ch2;
429  do
430  {
431 # pragma CPROVER check push
432 # pragma CPROVER check disable "conversion"
433  ch1=s1[i];
434  ch2=s2[i];
435 # pragma CPROVER check pop
436 
437  if(ch1>='A' && ch1<='Z') ch1+=('a'-'A');
438  if(ch2>='A' && ch2<='Z') ch2+=('a'-'A');
439 
440  if(ch1==ch2)
441  {
442  }
443  else if(ch1<ch2)
444  return -1;
445  else
446  return 1;
447 
448  i++;
449  }
450  while(ch1!=0 && ch2!=0);
451  return 0;
452 #endif
453 }
454 
455 /* FUNCTION: strncmp */
456 
457 #ifndef __CPROVER_STRING_H_INCLUDED
458 #include <string.h>
459 #define __CPROVER_STRING_H_INCLUDED
460 #endif
461 
462 #undef strncmp
463 
464 int strncmp(const char *s1, const char *s2, size_t n)
465 {
466 __CPROVER_HIDE:;
467 #ifdef __CPROVER_STRING_ABSTRACTION
468  __CPROVER_precondition(__CPROVER_is_zero_string(s1) ||
469  __CPROVER_buffer_size(s1)>=n,
470  "strncmp zero-termination of 1st argument");
471  __CPROVER_precondition(__CPROVER_is_zero_string(s2) ||
472  __CPROVER_buffer_size(s2)>=n,
473  "strncmp zero-termination of 2nd argument");
474 #else
475  __CPROVER_size_t i=0;
476  unsigned char ch1, ch2;
477  if(n == 0)
478  return 0;
479  do
480  {
481 # pragma CPROVER check push
482 # pragma CPROVER check disable "conversion"
483  ch1=s1[i];
484  ch2=s2[i];
485 # pragma CPROVER check pop
486 
487  if(ch1==ch2)
488  {
489  }
490  else if(ch1<ch2)
491  return -1;
492  else
493  return 1;
494 
495  i++;
496  }
497  while(ch1!=0 && ch2!=0 && i<n);
498  return 0;
499 #endif
500 }
501 
502 /* FUNCTION: strncasecmp */
503 
504 #ifndef __CPROVER_STRING_H_INCLUDED
505 #include <string.h>
506 #define __CPROVER_STRING_H_INCLUDED
507 #endif
508 
509 #undef strncasecmp
510 
511 int strncasecmp(const char *s1, const char *s2, size_t n)
512 {
513 __CPROVER_HIDE:;
514 #ifdef __CPROVER_STRING_ABSTRACTION
515  int retval;
516  __CPROVER_precondition(__CPROVER_is_zero_string(s1),
517  "strncasecmp zero-termination of 1st argument");
518  __CPROVER_precondition(__CPROVER_is_zero_string(s2),
519  "strncasecmp zero-termination of 2nd argument");
520  return retval;
521 #else
522  __CPROVER_size_t i=0;
523  unsigned char ch1, ch2;
524  if(n == 0)
525  return 0;
526  do
527  {
528 # pragma CPROVER check push
529 # pragma CPROVER check disable "conversion"
530  ch1=s1[i];
531  ch2=s2[i];
532 # pragma CPROVER check pop
533 
534  if(ch1>='A' && ch1<='Z') ch1+=('a'-'A');
535  if(ch2>='A' && ch2<='Z') ch2+=('a'-'A');
536 
537  if(ch1==ch2)
538  {
539  }
540  else if(ch1<ch2)
541  return -1;
542  else
543  return 1;
544 
545  i++;
546  }
547  while(ch1!=0 && ch2!=0 && i<n);
548  return 0;
549 #endif
550 }
551 
552 /* FUNCTION: strlen */
553 
554 #ifndef __CPROVER_STRING_H_INCLUDED
555 #include <string.h>
556 #define __CPROVER_STRING_H_INCLUDED
557 #endif
558 
559 #undef strlen
560 
561 size_t strlen(const char *s)
562 {
563  __CPROVER_HIDE:;
564  #ifdef __CPROVER_STRING_ABSTRACTION
565  __CPROVER_precondition(__CPROVER_is_zero_string(s),
566  "strlen zero-termination");
567  return __CPROVER_zero_string_length(s);
568  #else
569  __CPROVER_size_t len=0;
570  while(s[len]!=0) len++;
571  return len;
572  #endif
573 }
574 
575 /* FUNCTION: strdup */
576 
577 #ifndef __CPROVER_STRING_H_INCLUDED
578 #include <string.h>
579 #define __CPROVER_STRING_H_INCLUDED
580 #endif
581 
582 #ifndef __CPROVER_STDLIB_H_INCLUDED
583 #include <stdlib.h>
584 #define __CPROVER_STDLIB_H_INCLUDED
585 #endif
586 
587 #undef strdup
588 #undef strcpy
589 
590 char *strdup(const char *str)
591 {
592  __CPROVER_HIDE:;
593  __CPROVER_size_t bufsz;
594  bufsz=(strlen(str)+1);
595  char *cpy = (char *)calloc(bufsz * sizeof(char), sizeof(char));
596  if(cpy==((void *)0)) return 0;
597  #ifdef __CPROVER_STRING_ABSTRACTION
598  __CPROVER_assume(__CPROVER_buffer_size(cpy)==bufsz);
599  #endif
600  strcpy(cpy, str);
601  return cpy;
602 }
603 
604 /* FUNCTION: memcpy */
605 
606 #ifndef __CPROVER_STRING_H_INCLUDED
607 #include <string.h>
608 #define __CPROVER_STRING_H_INCLUDED
609 #endif
610 
611 #undef memcpy
612 
613 void *memcpy(void *dst, const void *src, size_t n)
614 {
615 __CPROVER_HIDE:;
616 
617 #ifdef __CPROVER_STRING_ABSTRACTION
618  __CPROVER_precondition(
619  __CPROVER_buffer_size(src) >= n, "memcpy buffer overflow");
620  __CPROVER_precondition(
621  __CPROVER_buffer_size(dst) >= n, "memcpy buffer overflow");
622  // for(size_t i=0; i<n ; i++) dst[i]=src[i];
623  if(__CPROVER_is_zero_string(src) && n > __CPROVER_zero_string_length(src))
624  {
625  __CPROVER_is_zero_string(dst) = 1;
626  __CPROVER_zero_string_length(dst) = __CPROVER_zero_string_length(src);
627  }
628  else if(!(__CPROVER_is_zero_string(dst) &&
629  n <= __CPROVER_zero_string_length(dst)))
630  {
631  __CPROVER_is_zero_string(dst) = 0;
632  }
633 
634 #else
635  __CPROVER_precondition(
636  __CPROVER_POINTER_OBJECT(dst) != __CPROVER_POINTER_OBJECT(src) ||
637  ((const char *)src >= (const char *)dst + n) ||
638  ((const char *)dst >= (const char *)src + n),
639  "memcpy src/dst overlap");
640  __CPROVER_precondition(
641  __CPROVER_r_ok(src, n), "memcpy source region readable");
642  __CPROVER_precondition(
643  __CPROVER_w_ok(dst, n), "memcpy destination region writeable");
644 
645  if(n > 0)
646  {
647  //for(__CPROVER_size_t i=0; i<n ; i++) ((char *)dst)[i]=((const char *)src)[i];
648  char src_n[n];
649  __CPROVER_array_copy(src_n, (char *)src);
650  __CPROVER_array_replace((char *)dst, src_n);
651  }
652 #endif
653 
654  return dst;
655 }
656 
657 /* FUNCTION: __builtin___memcpy_chk */
658 
659 void *__builtin___memcpy_chk(void *dst, const void *src, __CPROVER_size_t n, __CPROVER_size_t size)
660 {
661 __CPROVER_HIDE:
662 #ifdef __CPROVER_STRING_ABSTRACTION
663  __CPROVER_precondition(
664  __CPROVER_buffer_size(src) >= n, "memcpy buffer overflow");
665  __CPROVER_precondition(
666  __CPROVER_buffer_size(dst) >= n, "memcpy buffer overflow");
667  __CPROVER_precondition(
668  size == ~(__CPROVER_size_t)0 || __CPROVER_buffer_size(dst) == size,
669  "builtin object size");
670  // for(size_t i=0; i<n ; i++) dst[i]=src[i];
671  if(__CPROVER_is_zero_string(src) && n > __CPROVER_zero_string_length(src))
672  {
673  __CPROVER_is_zero_string(dst) = 1;
674  __CPROVER_zero_string_length(dst) = __CPROVER_zero_string_length(src);
675  }
676  else if(!(__CPROVER_is_zero_string(dst) &&
677  n <= __CPROVER_zero_string_length(dst)))
678  {
679  __CPROVER_is_zero_string(dst) = 0;
680  }
681 #else
682  __CPROVER_precondition(
683  __CPROVER_POINTER_OBJECT(dst) != __CPROVER_POINTER_OBJECT(src) ||
684  ((const char *)src >= (const char *)dst + n) ||
685  ((const char *)dst >= (const char *)src + n),
686  "memcpy src/dst overlap");
687  __CPROVER_precondition(
688  __CPROVER_r_ok(src, n), "memcpy source region readable");
689  __CPROVER_precondition(
690  __CPROVER_w_ok(dst, n), "memcpy destination region writeable");
691  (void)size;
692 
693  if(n > 0)
694  {
695  //for(__CPROVER_size_t i=0; i<n ; i++) ((char *)dst)[i]=((const char *)src)[i];
696  char src_n[n];
697  __CPROVER_array_copy(src_n, (char *)src);
698  __CPROVER_array_replace((char *)dst, src_n);
699  }
700 #endif
701  return dst;
702 }
703 
704 /* FUNCTION: memset */
705 
706 #ifndef __CPROVER_STRING_H_INCLUDED
707 #include <string.h>
708 #define __CPROVER_STRING_H_INCLUDED
709 #endif
710 
711 #undef memset
712 
713 void *memset(void *s, int c, size_t n)
714 {
715  __CPROVER_HIDE:;
716  #ifdef __CPROVER_STRING_ABSTRACTION
717  __CPROVER_precondition(__CPROVER_buffer_size(s)>=n,
718  "memset buffer overflow");
719  // for(size_t i=0; i<n ; i++) s[i]=c;
720  if(__CPROVER_is_zero_string(s) &&
721  n > __CPROVER_zero_string_length(s))
722  {
723  __CPROVER_is_zero_string(s)=1;
724  }
725  else if(c==0)
726  {
727  __CPROVER_is_zero_string(s)=1;
728  __CPROVER_zero_string_length(s)=0;
729  }
730  else
731  __CPROVER_is_zero_string(s)=0;
732  #else
733  __CPROVER_precondition(__CPROVER_w_ok(s, n),
734  "memset destination region writeable");
735 
736  if(n > 0)
737  {
738  //char *sp=s;
739  //for(__CPROVER_size_t i=0; i<n ; i++) sp[i]=c;
740  unsigned char s_n[n];
741  __CPROVER_array_set(s_n, (unsigned char)c);
742  __CPROVER_array_replace((unsigned char *)s, s_n);
743  }
744  #endif
745  return s;
746 }
747 
748 /* FUNCTION: __builtin_memset */
749 
750 void *__builtin_memset(void *s, int c, __CPROVER_size_t n)
751 {
752  __CPROVER_HIDE:;
753  #ifdef __CPROVER_STRING_ABSTRACTION
754  __CPROVER_precondition(__CPROVER_buffer_size(s)>=n,
755  "memset buffer overflow");
756  // for(size_t i=0; i<n ; i++) s[i]=c;
757  if(__CPROVER_is_zero_string(s) &&
758  n > __CPROVER_zero_string_length(s))
759  {
760  __CPROVER_is_zero_string(s)=1;
761  }
762  else if(c==0)
763  {
764  __CPROVER_is_zero_string(s)=1;
765  __CPROVER_zero_string_length(s)=0;
766  }
767  else
768  {
769  __CPROVER_is_zero_string(s)=0;
770  }
771  #else
772  __CPROVER_precondition(__CPROVER_w_ok(s, n),
773  "memset destination region writeable");
774 
775  if(n > 0)
776  {
777  //char *sp=s;
778  //for(__CPROVER_size_t i=0; i<n ; i++) sp[i]=c;
779  unsigned char s_n[n];
780  __CPROVER_array_set(s_n, (unsigned char)c);
781  __CPROVER_array_replace((unsigned char *)s, s_n);
782  }
783  #endif
784  return s;
785 }
786 
787 /* FUNCTION: __builtin___memset_chk */
788 
789 void *__builtin___memset_chk(void *s, int c, __CPROVER_size_t n, __CPROVER_size_t size)
790 {
791 __CPROVER_HIDE:;
792 #ifdef __CPROVER_STRING_ABSTRACTION
793  __CPROVER_precondition(__CPROVER_buffer_size(s)>=n,
794  "memset buffer overflow");
795  __CPROVER_precondition(
796  size == ~(__CPROVER_size_t)0 || __CPROVER_buffer_size(s) == size,
797  "builtin object size");
798  // for(size_t i=0; i<n ; i++) s[i]=c;
799  if(__CPROVER_is_zero_string(s) &&
800  n > __CPROVER_zero_string_length(s))
801  {
802  __CPROVER_is_zero_string(s)=1;
803  }
804  else if(c==0)
805  {
806  __CPROVER_is_zero_string(s)=1;
807  __CPROVER_zero_string_length(s)=0;
808  }
809  else
810  __CPROVER_is_zero_string(s)=0;
811 #else
812  __CPROVER_precondition(__CPROVER_w_ok(s, n),
813  "memset destination region writeable");
814  (void)size;
815 
816  if(n > 0)
817  {
818  //char *sp=s;
819  //for(__CPROVER_size_t i=0; i<n ; i++) sp[i]=c;
820  unsigned char s_n[n];
821  __CPROVER_array_set(s_n, (unsigned char)c);
822  __CPROVER_array_replace((unsigned char *)s, s_n);
823  }
824 #endif
825  return s;
826 }
827 
828 /* FUNCTION: memmove */
829 
830 #ifndef __CPROVER_STRING_H_INCLUDED
831 #include <string.h>
832 #define __CPROVER_STRING_H_INCLUDED
833 #endif
834 
835 #undef memmove
836 
837 void *memmove(void *dest, const void *src, size_t n)
838 {
839  __CPROVER_HIDE:;
840  #ifdef __CPROVER_STRING_ABSTRACTION
841  __CPROVER_precondition(__CPROVER_buffer_size(src)>=n,
842  "memmove buffer overflow");
843  // dst = src (with overlap allowed)
844  if(__CPROVER_is_zero_string(src) &&
845  n > __CPROVER_zero_string_length(src))
846  {
847  __CPROVER_is_zero_string(src)=1;
848  __CPROVER_zero_string_length(dest)=__CPROVER_zero_string_length(src);
849  }
850  else
851  __CPROVER_is_zero_string(dest)=0;
852  #else
853  __CPROVER_precondition(__CPROVER_r_ok(src, n),
854  "memmove source region readable");
855  __CPROVER_precondition(__CPROVER_w_ok(dest, n),
856  "memmove destination region writeable");
857 
858  if(n > 0)
859  {
860  char src_n[n];
861  __CPROVER_array_copy(src_n, (char *)src);
862  __CPROVER_array_replace((char *)dest, src_n);
863  }
864  #endif
865  return dest;
866 }
867 
868 /* FUNCTION: __builtin___memmove_chk */
869 
870 #ifndef __CPROVER_STRING_H_INCLUDED
871 #include <string.h>
872 #define __CPROVER_STRING_H_INCLUDED
873 #endif
874 
875 #undef memmove
876 
877 void *__builtin___memmove_chk(void *dest, const void *src, size_t n, __CPROVER_size_t size)
878 {
879  __CPROVER_HIDE:;
880  #ifdef __CPROVER_STRING_ABSTRACTION
881  __CPROVER_precondition(__CPROVER_buffer_size(src)>=n,
882  "memmove buffer overflow");
883  __CPROVER_precondition(
884  size == ~(__CPROVER_size_t)0 || __CPROVER_buffer_size(dest) == size,
885  "builtin object size");
886  // dst = src (with overlap allowed)
887  if(__CPROVER_is_zero_string(src) &&
888  n > __CPROVER_zero_string_length(src))
889  {
890  __CPROVER_is_zero_string(src)=1;
891  __CPROVER_zero_string_length(dest)=__CPROVER_zero_string_length(src);
892  }
893  else
894  {
895  __CPROVER_is_zero_string(dest)=0;
896  }
897  #else
898  __CPROVER_precondition(__CPROVER_r_ok(src, n),
899  "memmove source region readable");
900  __CPROVER_precondition(__CPROVER_w_ok(dest, n),
901  "memmove destination region writeable");
902  (void)size;
903 
904  if(n > 0)
905  {
906  char src_n[n];
907  __CPROVER_array_copy(src_n, (char *)src);
908  __CPROVER_array_replace((char *)dest, src_n);
909  }
910  #endif
911  return dest;
912 }
913 
914 /* FUNCTION: memcmp */
915 
916 #ifndef __CPROVER_STRING_H_INCLUDED
917 #include <string.h>
918 #define __CPROVER_STRING_H_INCLUDED
919 #endif
920 
921 #undef memcmp
922 
923 int memcmp(const void *s1, const void *s2, size_t n)
924 {
925  __CPROVER_HIDE:;
926  int res=0;
927  #ifdef __CPROVER_STRING_ABSTRACTION
928  __CPROVER_precondition(__CPROVER_buffer_size(s1)>=n,
929  "memcmp buffer overflow of 1st argument");
930  __CPROVER_precondition(__CPROVER_buffer_size(s2)>=n,
931  "memcmp buffer overflow of 2nd argument");
932  #else
933  __CPROVER_precondition(__CPROVER_r_ok(s1, n),
934  "memcmp region 1 readable");
935  __CPROVER_precondition(__CPROVER_r_ok(s2, n),
936  "memcpy region 2 readable");
937 
938  const unsigned char *sc1=s1, *sc2=s2;
939  for(; n!=0; n--)
940  {
941  res = (*sc1++) - (*sc2++);
942  if (res != 0)
943  return res;
944  }
945  #endif
946  return res;
947 }
948 
949 /* FUNCTION: strchr */
950 
951 #ifndef __CPROVER_STRING_H_INCLUDED
952 #include <string.h>
953 #define __CPROVER_STRING_H_INCLUDED
954 #endif
955 
956 #undef strchr
957 
958 char *strchr(const char *src, int c)
959 {
960  __CPROVER_HIDE:;
961  #ifdef __CPROVER_STRING_ABSTRACTION
962  __CPROVER_precondition(__CPROVER_is_zero_string(src),
963  "strchr zero-termination of string argument");
964  __CPROVER_bool found;
965  __CPROVER_size_t i;
966  return found?src+i:0;
967  #else
968  for(__CPROVER_size_t i=0; ; i++)
969  {
970  if(src[i]==(char)c)
971  return ((char *)src)+i; // cast away const-ness
972  if(src[i]==0) break;
973  }
974  return 0;
975  #endif
976 }
977 
978 /* FUNCTION: strrchr */
979 
980 #ifndef __CPROVER_STRING_H_INCLUDED
981 #include <string.h>
982 #define __CPROVER_STRING_H_INCLUDED
983 #endif
984 
985 #undef strchr
986 
987 char *strrchr(const char *src, int c)
988 {
989  __CPROVER_HIDE:;
990  #ifdef __CPROVER_STRING_ABSTRACTION
991  __CPROVER_precondition(__CPROVER_is_zero_string(src),
992  "strrchr zero-termination of string argument");
993  __CPROVER_bool found;
994  __CPROVER_size_t i;
995  return found?((char *)src)+i:0;
996  #else
997  char *res=0;
998  for(__CPROVER_size_t i=0; ; i++)
999  {
1000  if(src[i]==(char)c) res=((char *)src)+i;
1001  if(src[i]==0) break;
1002  }
1003  return res;
1004  #endif
1005 }
1006 
1007 /* FUNCTION: strerror */
1008 
1009 #ifndef __CPROVER_STRING_H_INCLUDED
1010 #include <string.h>
1011 #define __CPROVER_STRING_H_INCLUDED
1012 #endif
1013 
1014 char *strerror(int errnum)
1015 {
1016  __CPROVER_HIDE:;
1017  (void)errnum;
1018  #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
1019  __CPROVER_event("invalidate_pointer", "strerror_result");
1020  char *strerror_result;
1021  __CPROVER_set_must(strerror_result, "strerror_result");
1022  return strerror_result;
1023  #else
1024  static char strerror_result[1];
1025  return strerror_result;
1026  #endif
1027 }
__CPROVER_w_ok
__CPROVER_bool __CPROVER_w_ok(const void *,...)
__CPROVER_r_ok
__CPROVER_bool __CPROVER_r_ok(const void *,...)
s2
int16_t s2
Definition: bytecode_info.h:60
s1
int8_t s1
Definition: bytecode_info.h:59
__CPROVER_buffer_size
__CPROVER_size_t __CPROVER_buffer_size(const void *)
__CPROVER_assert
void __CPROVER_assert(__CPROVER_bool assertion, const char *description)
__CPROVER_array_replace
void __CPROVER_array_replace(const void *dest, const void *src)
__CPROVER_array_set
void __CPROVER_array_set(const void *dest,...)
__CPROVER_POINTER_OBJECT
__CPROVER_size_t __CPROVER_POINTER_OBJECT(const void *)
__CPROVER_zero_string_length
__CPROVER_size_t __CPROVER_zero_string_length(const void *)
__CPROVER_precondition
void __CPROVER_precondition(__CPROVER_bool precondition, const char *description)
__CPROVER_is_zero_string
_Bool __CPROVER_is_zero_string(const void *)
__CPROVER_set_must
void __CPROVER_set_must(const void *, const char *)
__CPROVER_assume
void __CPROVER_assume(__CPROVER_bool assumption)
__CPROVER_array_copy
void __CPROVER_array_copy(const void *dest, const void *src)
object_size
exprt object_size(const exprt &pointer)
Definition: pointer_predicates.cpp:33
calloc
void * calloc(__CPROVER_size_t nmemb, __CPROVER_size_t size)
Definition: stdlib.c:146
strncmp
int strncmp(const char *s1, const char *s2, size_t n)
Definition: string.c:464
strcmp
int strcmp(const char *s1, const char *s2)
Definition: string.c:363
memcpy
void * memcpy(void *dst, const void *src, size_t n)
Definition: string.c:613
strcpy
char * strcpy(char *dst, const char *src)
Definition: string.c:139
__builtin_memset
void * __builtin_memset(void *s, int c, __CPROVER_size_t n)
Definition: string.c:750
strdup
char * strdup(const char *str)
Definition: string.c:590
__builtin___strcpy_chk
char * __builtin___strcpy_chk(char *dst, const char *src, __CPROVER_size_t s)
Definition: string.c:3
strchr
char * strchr(const char *src, int c)
Definition: string.c:958
strcat
char * strcat(char *dst, const char *src)
Definition: string.c:262
strrchr
char * strrchr(const char *src, int c)
Definition: string.c:987
__builtin___memmove_chk
void * __builtin___memmove_chk(void *dest, const void *src, size_t n, __CPROVER_size_t size)
Definition: string.c:877
strncat
char * strncat(char *dst, const char *src, size_t n)
Definition: string.c:308
__builtin___memcpy_chk
void * __builtin___memcpy_chk(void *dst, const void *src, __CPROVER_size_t n, __CPROVER_size_t size)
Definition: string.c:659
strncasecmp
int strncasecmp(const char *s1, const char *s2, size_t n)
Definition: string.c:511
strcasecmp
int strcasecmp(const char *s1, const char *s2)
Definition: string.c:412
memmove
void * memmove(void *dest, const void *src, size_t n)
Definition: string.c:837
__builtin___strncpy_chk
char * __builtin___strncpy_chk(char *dst, const char *src, size_t n, size_t object_size)
Definition: string.c:214
memcmp
int memcmp(const void *s1, const void *s2, size_t n)
Definition: string.c:923
strlen
size_t strlen(const char *s)
Definition: string.c:561
__builtin___memset_chk
void * __builtin___memset_chk(void *s, int c, __CPROVER_size_t n, __CPROVER_size_t size)
Definition: string.c:789
__builtin___strncat_chk
__inline char * __builtin___strncat_chk(char *dst, const char *src, __CPROVER_size_t n, __CPROVER_size_t s)
Definition: string.c:81
memset
void * memset(void *s, int c, size_t n)
Definition: string.c:713
__builtin___strcat_chk
__inline char * __builtin___strcat_chk(char *dst, const char *src, __CPROVER_size_t s)
Definition: string.c:37
strncpy
char * strncpy(char *dst, const char *src, size_t n)
Definition: string.c:176
strerror
char * strerror(int errnum)
Definition: string.c:1014