CBMC
Loading...
Searching...
No Matches
string.c
Go to the documentation of this file.
1/* FUNCTION: __builtin___strcpy_chk */
2
3char *__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
139char *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
176char *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
214char *__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
262char *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
308char *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
363int 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
412int 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
464int 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
511int 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
561size_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
590char *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
613void *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 unsigned char *)src >= (const unsigned char *)dst + n) ||
638 ((const unsigned char *)dst >= (const unsigned 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++)
648 // ((unsigned char *)dst)[i]=((const unsigned char *)src)[i];
649 unsigned char src_n[n];
650 __CPROVER_array_copy(src_n, (unsigned char *)src);
651 __CPROVER_array_replace((unsigned char *)dst, src_n);
652 }
653#endif
654
655 return dst;
656}
657
658/* FUNCTION: __builtin___memcpy_chk */
659
660void *__builtin___memcpy_chk(void *dst, const void *src, __CPROVER_size_t n, __CPROVER_size_t size)
661{
662__CPROVER_HIDE:
663#ifdef __CPROVER_STRING_ABSTRACTION
664 __CPROVER_precondition(
665 __CPROVER_buffer_size(src) >= n, "memcpy buffer overflow");
666 __CPROVER_precondition(
667 __CPROVER_buffer_size(dst) >= n, "memcpy buffer overflow");
668 __CPROVER_precondition(
669 size == ~(__CPROVER_size_t)0 || __CPROVER_buffer_size(dst) == size,
670 "builtin object size");
671 // for(size_t i=0; i<n ; i++) dst[i]=src[i];
672 if(__CPROVER_is_zero_string(src) && n > __CPROVER_zero_string_length(src))
673 {
674 __CPROVER_is_zero_string(dst) = 1;
675 __CPROVER_zero_string_length(dst) = __CPROVER_zero_string_length(src);
676 }
677 else if(!(__CPROVER_is_zero_string(dst) &&
678 n <= __CPROVER_zero_string_length(dst)))
679 {
680 __CPROVER_is_zero_string(dst) = 0;
681 }
682#else
683 __CPROVER_precondition(
684 __CPROVER_POINTER_OBJECT(dst) != __CPROVER_POINTER_OBJECT(src) ||
685 ((const unsigned char *)src >= (const unsigned char *)dst + n) ||
686 ((const unsigned char *)dst >= (const unsigned char *)src + n),
687 "memcpy src/dst overlap");
688 __CPROVER_precondition(
689 __CPROVER_r_ok(src, n), "memcpy source region readable");
690 __CPROVER_precondition(
691 __CPROVER_w_ok(dst, n), "memcpy destination region writeable");
692 (void)size;
693
694 if(n > 0)
695 {
696 //for(__CPROVER_size_t i=0; i<n ; i++)
697 // ((unsigned char *)dst)[i]=((const unsigned char *)src)[i];
698 unsigned char src_n[n];
699 __CPROVER_array_copy(src_n, (unsigned char *)src);
700 __CPROVER_array_replace((unsigned char *)dst, src_n);
701 }
702#endif
703 return dst;
704}
705
706/* FUNCTION: memset */
707
708#ifndef __CPROVER_STRING_H_INCLUDED
709#include <string.h>
710#define __CPROVER_STRING_H_INCLUDED
711#endif
712
713#undef memset
714
715void *memset(void *s, int c, size_t n)
716{
717 __CPROVER_HIDE:;
718 #ifdef __CPROVER_STRING_ABSTRACTION
719 __CPROVER_precondition(__CPROVER_buffer_size(s)>=n,
720 "memset buffer overflow");
721 // for(size_t i=0; i<n ; i++) s[i]=c;
722 if(__CPROVER_is_zero_string(s) &&
723 n > __CPROVER_zero_string_length(s))
724 {
725 __CPROVER_is_zero_string(s)=1;
726 }
727 else if(c==0)
728 {
729 __CPROVER_is_zero_string(s)=1;
730 __CPROVER_zero_string_length(s)=0;
731 }
732 else
733 __CPROVER_is_zero_string(s)=0;
734 #else
735 __CPROVER_precondition(__CPROVER_w_ok(s, n),
736 "memset destination region writeable");
737
738 if(n > 0)
739 {
740 //char *sp=s;
741 //for(__CPROVER_size_t i=0; i<n ; i++) sp[i]=c;
742 unsigned char s_n[n];
743 __CPROVER_array_set(s_n, (unsigned char)c);
744 __CPROVER_array_replace((unsigned char *)s, s_n);
745 }
746 #endif
747 return s;
748}
749
750/* FUNCTION: __builtin_memset */
751
752void *__builtin_memset(void *s, int c, __CPROVER_size_t n)
753{
754 __CPROVER_HIDE:;
755 #ifdef __CPROVER_STRING_ABSTRACTION
756 __CPROVER_precondition(__CPROVER_buffer_size(s)>=n,
757 "memset buffer overflow");
758 // for(size_t i=0; i<n ; i++) s[i]=c;
759 if(__CPROVER_is_zero_string(s) &&
760 n > __CPROVER_zero_string_length(s))
761 {
762 __CPROVER_is_zero_string(s)=1;
763 }
764 else if(c==0)
765 {
766 __CPROVER_is_zero_string(s)=1;
767 __CPROVER_zero_string_length(s)=0;
768 }
769 else
770 {
771 __CPROVER_is_zero_string(s)=0;
772 }
773 #else
774 __CPROVER_precondition(__CPROVER_w_ok(s, n),
775 "memset destination region writeable");
776
777 if(n > 0)
778 {
779 //char *sp=s;
780 //for(__CPROVER_size_t i=0; i<n ; i++) sp[i]=c;
781 unsigned char s_n[n];
782 __CPROVER_array_set(s_n, (unsigned char)c);
783 __CPROVER_array_replace((unsigned char *)s, s_n);
784 }
785 #endif
786 return s;
787}
788
789/* FUNCTION: __builtin___memset_chk */
790
791void *__builtin___memset_chk(void *s, int c, __CPROVER_size_t n, __CPROVER_size_t size)
792{
793__CPROVER_HIDE:;
794#ifdef __CPROVER_STRING_ABSTRACTION
795 __CPROVER_precondition(__CPROVER_buffer_size(s)>=n,
796 "memset buffer overflow");
797 __CPROVER_precondition(
798 size == ~(__CPROVER_size_t)0 || __CPROVER_buffer_size(s) == size,
799 "builtin object size");
800 // for(size_t i=0; i<n ; i++) s[i]=c;
801 if(__CPROVER_is_zero_string(s) &&
802 n > __CPROVER_zero_string_length(s))
803 {
804 __CPROVER_is_zero_string(s)=1;
805 }
806 else if(c==0)
807 {
808 __CPROVER_is_zero_string(s)=1;
809 __CPROVER_zero_string_length(s)=0;
810 }
811 else
812 __CPROVER_is_zero_string(s)=0;
813#else
814 __CPROVER_precondition(__CPROVER_w_ok(s, n),
815 "memset destination region writeable");
816 (void)size;
817
818 if(n > 0)
819 {
820 //char *sp=s;
821 //for(__CPROVER_size_t i=0; i<n ; i++) sp[i]=c;
822 unsigned char s_n[n];
823 __CPROVER_array_set(s_n, (unsigned char)c);
824 __CPROVER_array_replace((unsigned char *)s, s_n);
825 }
826#endif
827 return s;
828}
829
830/* FUNCTION: memmove */
831
832#ifndef __CPROVER_STRING_H_INCLUDED
833#include <string.h>
834#define __CPROVER_STRING_H_INCLUDED
835#endif
836
837#undef memmove
838
839void *memmove(void *dest, const void *src, size_t n)
840{
841 __CPROVER_HIDE:;
842 #ifdef __CPROVER_STRING_ABSTRACTION
843 __CPROVER_precondition(__CPROVER_buffer_size(src)>=n,
844 "memmove buffer overflow");
845 // dst = src (with overlap allowed)
846 if(__CPROVER_is_zero_string(src) &&
847 n > __CPROVER_zero_string_length(src))
848 {
849 __CPROVER_is_zero_string(src)=1;
850 __CPROVER_zero_string_length(dest)=__CPROVER_zero_string_length(src);
851 }
852 else
853 __CPROVER_is_zero_string(dest)=0;
854 #else
855 __CPROVER_precondition(__CPROVER_r_ok(src, n),
856 "memmove source region readable");
857 __CPROVER_precondition(__CPROVER_w_ok(dest, n),
858 "memmove destination region writeable");
859
860 if(n > 0)
861 {
862 unsigned char src_n[n];
863 __CPROVER_array_copy(src_n, (unsigned char *)src);
864 __CPROVER_array_replace((unsigned char *)dest, src_n);
865 }
866 #endif
867 return dest;
868}
869
870/* FUNCTION: __builtin___memmove_chk */
871
872#ifndef __CPROVER_STRING_H_INCLUDED
873#include <string.h>
874#define __CPROVER_STRING_H_INCLUDED
875#endif
876
877#undef memmove
878
879void *__builtin___memmove_chk(void *dest, const void *src, size_t n, __CPROVER_size_t size)
880{
881 __CPROVER_HIDE:;
882 #ifdef __CPROVER_STRING_ABSTRACTION
883 __CPROVER_precondition(__CPROVER_buffer_size(src)>=n,
884 "memmove buffer overflow");
885 __CPROVER_precondition(
886 size == ~(__CPROVER_size_t)0 || __CPROVER_buffer_size(dest) == size,
887 "builtin object size");
888 // dst = src (with overlap allowed)
889 if(__CPROVER_is_zero_string(src) &&
890 n > __CPROVER_zero_string_length(src))
891 {
892 __CPROVER_is_zero_string(src)=1;
893 __CPROVER_zero_string_length(dest)=__CPROVER_zero_string_length(src);
894 }
895 else
896 {
897 __CPROVER_is_zero_string(dest)=0;
898 }
899 #else
900 __CPROVER_precondition(__CPROVER_r_ok(src, n),
901 "memmove source region readable");
902 __CPROVER_precondition(__CPROVER_w_ok(dest, n),
903 "memmove destination region writeable");
904 (void)size;
905
906 if(n > 0)
907 {
908 unsigned char src_n[n];
909 __CPROVER_array_copy(src_n, (unsigned char *)src);
910 __CPROVER_array_replace((unsigned char *)dest, src_n);
911 }
912 #endif
913 return dest;
914}
915
916/* FUNCTION: memcmp */
917
918#ifndef __CPROVER_STRING_H_INCLUDED
919#include <string.h>
920#define __CPROVER_STRING_H_INCLUDED
921#endif
922
923#undef memcmp
924
925int memcmp(const void *s1, const void *s2, size_t n)
926{
927 __CPROVER_HIDE:;
928 int res=0;
929 #ifdef __CPROVER_STRING_ABSTRACTION
930 __CPROVER_precondition(__CPROVER_buffer_size(s1)>=n,
931 "memcmp buffer overflow of 1st argument");
932 __CPROVER_precondition(__CPROVER_buffer_size(s2)>=n,
933 "memcmp buffer overflow of 2nd argument");
934 #else
935 __CPROVER_precondition(__CPROVER_r_ok(s1, n),
936 "memcmp region 1 readable");
937 __CPROVER_precondition(__CPROVER_r_ok(s2, n),
938 "memcpy region 2 readable");
939
940 const unsigned char *sc1=s1, *sc2=s2;
941 for(; n!=0; n--)
942 {
943 res = (*sc1++) - (*sc2++);
944 if (res != 0)
945 return res;
946 }
947 #endif
948 return res;
949}
950
951/* FUNCTION: strchr */
952
953#ifndef __CPROVER_STRING_H_INCLUDED
954#include <string.h>
955#define __CPROVER_STRING_H_INCLUDED
956#endif
957
958#undef strchr
959
960char *strchr(const char *src, int c)
961{
962 __CPROVER_HIDE:;
963 #ifdef __CPROVER_STRING_ABSTRACTION
964 __CPROVER_precondition(__CPROVER_is_zero_string(src),
965 "strchr zero-termination of string argument");
966 __CPROVER_bool found;
967 __CPROVER_size_t i;
968 return found?src+i:0;
969 #else
970 for(__CPROVER_size_t i=0; ; i++)
971 {
972 if(src[i]==(char)c)
973 return ((char *)src)+i; // cast away const-ness
974 if(src[i]==0) break;
975 }
976 return 0;
977 #endif
978}
979
980/* FUNCTION: strrchr */
981
982#ifndef __CPROVER_STRING_H_INCLUDED
983#include <string.h>
984#define __CPROVER_STRING_H_INCLUDED
985#endif
986
987#undef strchr
988
989char *strrchr(const char *src, int c)
990{
991 __CPROVER_HIDE:;
992 #ifdef __CPROVER_STRING_ABSTRACTION
993 __CPROVER_precondition(__CPROVER_is_zero_string(src),
994 "strrchr zero-termination of string argument");
995 __CPROVER_bool found;
996 __CPROVER_size_t i;
997 return found?((char *)src)+i:0;
998 #else
999 char *res=0;
1000 for(__CPROVER_size_t i=0; ; i++)
1001 {
1002 if(src[i]==(char)c) res=((char *)src)+i;
1003 if(src[i]==0) break;
1004 }
1005 return res;
1006 #endif
1007}
1008
1009/* FUNCTION: strerror */
1010
1011#ifndef __CPROVER_STRING_H_INCLUDED
1012#include <string.h>
1013#define __CPROVER_STRING_H_INCLUDED
1014#endif
1015
1016char *strerror(int errnum)
1017{
1018 __CPROVER_HIDE:;
1019 (void)errnum;
1020 #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
1021 __CPROVER_event("invalidate_pointer", "strerror_result");
1022 char *strerror_result;
1023 __CPROVER_set_must(strerror_result, "strerror_result");
1024 return strerror_result;
1025 #else
1026 static char strerror_result[1];
1027 return strerror_result;
1028 #endif
1029}
__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
__builtin___strcpy_chk
char * __builtin___strcpy_chk(char *dst, const char *src, __CPROVER_size_t s)
Definition string.c:3
strcmp
int strcmp(const char *s1, const char *s2)
Definition string.c:363
memset
void * memset(void *s, int c, size_t n)
Definition string.c:715
__builtin___memcpy_chk
void * __builtin___memcpy_chk(void *dst, const void *src, __CPROVER_size_t n, __CPROVER_size_t size)
Definition string.c:660
memmove
void * memmove(void *dest, const void *src, size_t n)
Definition string.c:839
__builtin___memset_chk
void * __builtin___memset_chk(void *s, int c, __CPROVER_size_t n, __CPROVER_size_t size)
Definition string.c:791
strerror
char * strerror(int errnum)
Definition string.c:1016
__builtin___strcat_chk
__inline char * __builtin___strcat_chk(char *dst, const char *src, __CPROVER_size_t s)
Definition string.c:37
__builtin___strncpy_chk
char * __builtin___strncpy_chk(char *dst, const char *src, size_t n, size_t object_size)
Definition string.c:214
strcpy
char * strcpy(char *dst, const char *src)
Definition string.c:139
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
__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
strrchr
char * strrchr(const char *src, int c)
Definition string.c:989
strncpy
char * strncpy(char *dst, const char *src, size_t n)
Definition string.c:176
__builtin_memset
void * __builtin_memset(void *s, int c, __CPROVER_size_t n)
Definition string.c:752
strcat
char * strcat(char *dst, const char *src)
Definition string.c:262
memcmp
int memcmp(const void *s1, const void *s2, size_t n)
Definition string.c:925
strchr
char * strchr(const char *src, int c)
Definition string.c:960
strlen
size_t strlen(const char *s)
Definition string.c:561
memcpy
void * memcpy(void *dst, const void *src, size_t n)
Definition string.c:613
__builtin___memmove_chk
void * __builtin___memmove_chk(void *dest, const void *src, size_t n, __CPROVER_size_t size)
Definition string.c:879
strdup
char * strdup(const char *str)
Definition string.c:590
strncat
char * strncat(char *dst, const char *src, size_t n)
Definition string.c:308