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 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
659void *__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
713void *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
750void *__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
789void *__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
837void *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
877void *__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
923int 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
958char *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
987char *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
1014char *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
ait
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
__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:713
__builtin___memcpy_chk
void * __builtin___memcpy_chk(void *dst, const void *src, __CPROVER_size_t n, __CPROVER_size_t size)
Definition string.c:659
memmove
void * memmove(void *dest, const void *src, size_t n)
Definition string.c:837
__builtin___memset_chk
void * __builtin___memset_chk(void *s, int c, __CPROVER_size_t n, __CPROVER_size_t size)
Definition string.c:789
strerror
char * strerror(int errnum)
Definition string.c:1014
__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:987
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:750
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:923
strchr
char * strchr(const char *src, int c)
Definition string.c:958
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:877
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