CBMC: /home/runner/work/cbmc/cbmc/src/ansi-c/library/string.c Source File

CBMC
Loading...
Searching...
No Matches
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{
6
7#ifdef __CPROVER_STRING_ABSTRACTION
9 __CPROVER_is_zero_string(src), "strcpy zero-termination of 2nd argument");
12 "strcpy buffer overflow");
15 "builtin object size");
19#else
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{
40
41#ifdef __CPROVER_STRING_ABSTRACTION
44 __CPROVER_is_zero_string(dst), "strcat zero-termination of 1st argument");
46 __CPROVER_is_zero_string(src), "strcat zero-termination of 2nd argument");
49 "builtin object size");
50 new_size =
53 __CPROVER_buffer_size(dst) > new_size, "strcat buffer overflow");
55 //" for(size_t i=0; i<__CPROVER_zero_string_length(src); i++)
56 //" dst[old_size+i];
57 dst[new_size] = 0;
60#else
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
82 char *dst, const char *src, __CPROVER_size_t n, __CPROVER_size_t s)
83{
85#ifdef __CPROVER_STRING_ABSTRACTION
88 __CPROVER_is_zero_string(dst), "strncat zero-termination of 1st argument");
91 "strncat zero-termination of 2nd argument");
94 "builtin object size");
96 ? n
100 __CPROVER_buffer_size(dst) > new_size, "strncat buffer overflow");
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;
108#else
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{
142#ifdef __CPROVER_STRING_ABSTRACTION
144 __CPROVER_is_zero_string(src), "strcpy zero-termination of 2nd argument");
147 "strcpy buffer overflow");
151#else
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{
179#ifdef __CPROVER_STRING_ABSTRACTION
181 __CPROVER_is_zero_string(src), "strncpy zero-termination of 2nd argument");
183 __CPROVER_buffer_size(dst) >= n, "strncpy buffer overflow");
186#else
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
215 char *dst,
216 const char *src,
217 size_t n,
218 size_t object_size)
219{
221#ifdef __CPROVER_STRING_ABSTRACTION
223 __CPROVER_is_zero_string(src), "strncpy zero-termination of 2nd argument");
225 __CPROVER_buffer_size(dst) >= n, "strncpy buffer overflow");
228 "strncpy object size");
231#else
234 (src >= dst + n) || (dst >= src + n),
235 "strncpy src/dst overlap");
236 __CPROVER_size_t i = 0;
237 char ch;
238 _Bool end;
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{
265#ifdef __CPROVER_STRING_ABSTRACTION
268 "strcat zero-termination of 1st argument");
270 "strcat zero-termination of 2nd argument");
273 "strcat buffer overflow");
275 //" for(size_t i=0; i<__CPROVER_zero_string_length(src); i++)
276 //" dst[old_size+i];
277 dst[new_size]=0;
280#else
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{
311#ifdef __CPROVER_STRING_ABSTRACTION
314 __CPROVER_is_zero_string(dst), "strncat zero-termination of 1st argument");
317 "strncat zero-termination of 2nd argument");
319 ? n
323 __CPROVER_buffer_size(dst) > new_size, "strncat buffer overflow");
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;
331#else
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{
366#ifdef __CPROVER_STRING_ABSTRACTION
367 int retval;
369 "strcmp zero-termination of 1st argument");
371 "strcmp zero-termination of 2nd argument");
372
375
376 return retval;
377#else
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{
415#ifdef __CPROVER_STRING_ABSTRACTION
416 int retval;
418 "strcasecmp zero-termination of 1st argument");
420 "strcasecmp zero-termination of 2nd argument");
421
424
425 return retval;
426#else
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{
467#ifdef __CPROVER_STRING_ABSTRACTION
470 "strncmp zero-termination of 1st argument");
473 "strncmp zero-termination of 2nd argument");
474#else
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{
514#ifdef __CPROVER_STRING_ABSTRACTION
515 int retval;
517 "strncasecmp zero-termination of 1st argument");
519 "strncasecmp zero-termination of 2nd argument");
520 return retval;
521#else
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{
564 #ifdef __CPROVER_STRING_ABSTRACTION
566 "strlen zero-termination");
568 #else
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{
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
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{
616
617#ifdef __CPROVER_STRING_ABSTRACTION
619 __CPROVER_buffer_size(src) >= n, "memcpy buffer overflow");
621 __CPROVER_buffer_size(dst) >= n, "memcpy buffer overflow");
622 // for(size_t i=0; i<n ; i++) dst[i]=src[i];
624 {
627 }
628 else if(!(__CPROVER_is_zero_string(dst) &&
630 {
632 }
633
634#else
637 ((const char *)src >= (const char *)dst + n) ||
638 ((const char *)dst >= (const char *)src + n),
639 "memcpy src/dst overlap");
641 __CPROVER_r_ok(src, n), "memcpy source region readable");
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);
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{
662#ifdef __CPROVER_STRING_ABSTRACTION
664 __CPROVER_buffer_size(src) >= n, "memcpy buffer overflow");
666 __CPROVER_buffer_size(dst) >= n, "memcpy buffer overflow");
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];
672 {
675 }
676 else if(!(__CPROVER_is_zero_string(dst) &&
678 {
680 }
681#else
684 ((const char *)src >= (const char *)dst + n) ||
685 ((const char *)dst >= (const char *)src + n),
686 "memcpy src/dst overlap");
688 __CPROVER_r_ok(src, n), "memcpy source region readable");
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);
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{
716 #ifdef __CPROVER_STRING_ABSTRACTION
718 "memset buffer overflow");
719 // for(size_t i=0; i<n ; i++) s[i]=c;
722 {
724 }
725 else if(c==0)
726 {
729 }
730 else
732 #else
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
751{
753 #ifdef __CPROVER_STRING_ABSTRACTION
755 "memset buffer overflow");
756 // for(size_t i=0; i<n ; i++) s[i]=c;
759 {
761 }
762 else if(c==0)
763 {
766 }
767 else
768 {
770 }
771 #else
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
790{
792#ifdef __CPROVER_STRING_ABSTRACTION
794 "memset buffer overflow");
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;
801 {
803 }
804 else if(c==0)
805 {
808 }
809 else
811#else
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{
840 #ifdef __CPROVER_STRING_ABSTRACTION
842 "memmove buffer overflow");
843 // dst = src (with overlap allowed)
844 if(__CPROVER_is_zero_string(src) &&
846 {
849 }
850 else
852 #else
854 "memmove source region readable");
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{
880 #ifdef __CPROVER_STRING_ABSTRACTION
882 "memmove buffer overflow");
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) &&
889 {
892 }
893 else
894 {
896 }
897 #else
899 "memmove source region readable");
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{
926 int res=0;
927 #ifdef __CPROVER_STRING_ABSTRACTION
929 "memcmp buffer overflow of 1st argument");
931 "memcmp buffer overflow of 2nd argument");
932 #else
934 "memcmp region 1 readable");
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{
961 #ifdef __CPROVER_STRING_ABSTRACTION
963 "strchr zero-termination of string argument");
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{
990 #ifdef __CPROVER_STRING_ABSTRACTION
992 "strrchr zero-termination of string argument");
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{
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_bool __CPROVER_w_ok(const void *,...)
__CPROVER_bool __CPROVER_r_ok(const void *,...)
int16_t s2
Definition bytecode_info.h:60
int8_t s1
Definition bytecode_info.h:59
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:566
__CPROVER_size_t __CPROVER_buffer_size(const void *)
void __CPROVER_assert(__CPROVER_bool assertion, const char *description)
void __CPROVER_array_replace(const void *dest, const void *src)
void __CPROVER_array_set(const void *dest,...)
__CPROVER_size_t __CPROVER_POINTER_OBJECT(const void *)
__CPROVER_size_t __CPROVER_zero_string_length(const void *)
void __CPROVER_precondition(__CPROVER_bool precondition, const char *description)
_Bool __CPROVER_is_zero_string(const void *)
void __CPROVER_set_must(const void *, const char *)
void __CPROVER_assume(__CPROVER_bool assumption)
void __CPROVER_array_copy(const void *dest, const void *src)
exprt object_size(const exprt &pointer)
void * calloc(__CPROVER_size_t nmemb, __CPROVER_size_t size)
Definition stdlib.c:146
int strncmp(const char *s1, const char *s2, size_t n)
Definition string.c:464
char * __builtin___strcpy_chk(char *dst, const char *src, __CPROVER_size_t s)
Definition string.c:3
int strcmp(const char *s1, const char *s2)
Definition string.c:363
void * memset(void *s, int c, size_t n)
Definition string.c:713
void * __builtin___memcpy_chk(void *dst, const void *src, __CPROVER_size_t n, __CPROVER_size_t size)
Definition string.c:659
void * memmove(void *dest, const void *src, size_t n)
Definition string.c:837
void * __builtin___memset_chk(void *s, int c, __CPROVER_size_t n, __CPROVER_size_t size)
Definition string.c:789
char * strerror(int errnum)
Definition string.c:1014
__inline char * __builtin___strcat_chk(char *dst, const char *src, __CPROVER_size_t s)
Definition string.c:37
char * __builtin___strncpy_chk(char *dst, const char *src, size_t n, size_t object_size)
Definition string.c:214
char * strcpy(char *dst, const char *src)
Definition string.c:139
int strncasecmp(const char *s1, const char *s2, size_t n)
Definition string.c:511
int strcasecmp(const char *s1, const char *s2)
Definition string.c:412
__inline char * __builtin___strncat_chk(char *dst, const char *src, __CPROVER_size_t n, __CPROVER_size_t s)
Definition string.c:81
char * strrchr(const char *src, int c)
Definition string.c:987
char * strncpy(char *dst, const char *src, size_t n)
Definition string.c:176
void * __builtin_memset(void *s, int c, __CPROVER_size_t n)
Definition string.c:750
char * strcat(char *dst, const char *src)
Definition string.c:262
int memcmp(const void *s1, const void *s2, size_t n)
Definition string.c:923
char * strchr(const char *src, int c)
Definition string.c:958
size_t strlen(const char *s)
Definition string.c:561
void * memcpy(void *dst, const void *src, size_t n)
Definition string.c:613
void * __builtin___memmove_chk(void *dest, const void *src, size_t n, __CPROVER_size_t size)
Definition string.c:877
char * strdup(const char *str)
Definition string.c:590
char * strncat(char *dst, const char *src, size_t n)
Definition string.c:308

AltStyle によって変換されたページ (->オリジナル) /