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

CBMC
Loading...
Searching...
No Matches
stdio.c
Go to the documentation of this file.
1
2/* FUNCTION: putchar */
3
4#ifndef __CPROVER_STDIO_H_INCLUDED
5#include <stdio.h>
6 #define __CPROVER_STDIO_H_INCLUDED
7#endif
8
9/* undefine macros in OpenBSD's stdio.h that are problematic to the checker. */
10#if defined(__OpenBSD__)
11#undef getchar
12#undef putchar
13#undef getc
14#undef feof
15#undef ferror
16#undef fileno
17#endif
18
19 __CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
20
21 int putchar(int c)
22{
25 __CPROVER_printf("%c", c);
26 return (error?-1:c);
27}
28
29/* FUNCTION: puts */
30
31#ifndef __CPROVER_STDIO_H_INCLUDED
32#include <stdio.h>
33#define __CPROVER_STDIO_H_INCLUDED
34#endif
35
36__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
37 int __VERIFIER_nondet_int(void);
38
39 int puts(const char *s)
40{
44 __CPROVER_printf("%s\n", s);
45 if(error) ret=-1; else __CPROVER_assume(ret>=0);
46 return ret;
47}
48
49/* FUNCTION: fclose_cleanup */
50
51#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
52void fclose_cleanup(void *stream)
53{
54__CPROVER_HIDE:;
55 __CPROVER_assert(
56 !__CPROVER_get_must(stream, "open") || __CPROVER_get_must(stream, "closed"),
57 "resource leak: fopen file not closed");
58}
59#endif
60
61/* FUNCTION: fopen */
62
63#ifndef __CPROVER_STDIO_H_INCLUDED
64#include <stdio.h>
65#define __CPROVER_STDIO_H_INCLUDED
66#endif
67
68#ifndef __CPROVER_STDLIB_H_INCLUDED
69#include <stdlib.h>
70 #define __CPROVER_STDLIB_H_INCLUDED
71#endif
72
73 void fclose_cleanup(void *stream);
74__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
75FILE *fopen64(const char *filename, const char *mode);
76
77 FILE *fopen(const char *filename, const char *mode)
78{
80 return fopen64(filename, mode);
81}
82
83/* FUNCTION: _fopen */
84
85// This is for Apple; we cannot fall back to fopen as we need
86// header files to have a definition of FILE available; the same
87// header files rename fopen to _fopen and would thus yield
88// unbounded recursion.
89
90#ifndef __CPROVER_STDIO_H_INCLUDED
91# include <stdio.h>
92# define __CPROVER_STDIO_H_INCLUDED
93#endif
94
95#ifndef __CPROVER_STDLIB_H_INCLUDED
96# include <stdlib.h>
97# define __CPROVER_STDLIB_H_INCLUDED
98#endif
99
100void fclose_cleanup(void *stream);
101__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
102
103#ifdef __APPLE__
104FILE *_fopen(const char *filename, const char *mode)
105{
106__CPROVER_HIDE:;
107 (void)*filename;
108 (void)*mode;
109# ifdef __CPROVER_STRING_ABSTRACTION
110 __CPROVER_assert(
111 __CPROVER_is_zero_string(filename),
112 "fopen zero-termination of 1st argument");
113 __CPROVER_assert(
114 __CPROVER_is_zero_string(mode), "fopen zero-termination of 2nd argument");
115# endif
116
117 FILE *fopen_result;
118
119 __CPROVER_bool fopen_error = __VERIFIER_nondet___CPROVER_bool();
120
121 fopen_result = fopen_error ? NULL : malloc(sizeof(FILE));
122
123# ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
124 __CPROVER_set_must(fopen_result, "open");
125 __CPROVER_cleanup(fopen_result, fclose_cleanup);
126# endif
127
128 return fopen_result;
129}
130#endif
131
132/* FUNCTION: fopen64 */
133
134#ifndef __CPROVER_STDIO_H_INCLUDED
135# include <stdio.h>
136# define __CPROVER_STDIO_H_INCLUDED
137#endif
138
139#ifndef __CPROVER_STDLIB_H_INCLUDED
140# include <stdlib.h>
141# define __CPROVER_STDLIB_H_INCLUDED
142#endif
143
144void fclose_cleanup(void *stream);
145__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
146
147 FILE *fopen64(const char *filename, const char *mode)
148{
150 (void)*filename;
151 (void)*mode;
152#ifdef __CPROVER_STRING_ABSTRACTION
154 __CPROVER_is_zero_string(filename),
155 "fopen zero-termination of 1st argument");
157 __CPROVER_is_zero_string(mode), "fopen zero-termination of 2nd argument");
158#endif
159
161
163
164#if !defined(__linux__) || defined(__GLIBC__)
165 fopen_result = fopen_error ? NULL : malloc(sizeof(FILE));
166#else
167 // libraries need to expose the definition of FILE; this is the
168 // case for musl
169 fopen_result = fopen_error ? NULL : malloc(sizeof(int));
170#endif
171
172#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
175#endif
176
177 return fopen_result;
178}
179
180/* FUNCTION: freopen */
181
182#ifndef __CPROVER_STDIO_H_INCLUDED
183#include <stdio.h>
184#define __CPROVER_STDIO_H_INCLUDED
185#endif
186
187FILE *freopen64(const char *filename, const char *mode, FILE *f);
188
189 FILE *freopen(const char *filename, const char *mode, FILE *f)
190{
192 return freopen64(filename, mode, f);
193}
194
195/* FUNCTION: freopen64 */
196
197#ifndef __CPROVER_STDIO_H_INCLUDED
198# include <stdio.h>
199# define __CPROVER_STDIO_H_INCLUDED
200#endif
201
202 FILE *freopen64(const char *filename, const char *mode, FILE *f)
203{
205 (void)*filename;
206 (void)*mode;
207#if !defined(__linux__) || defined(__GLIBC__)
208 (void)*f;
209#else
210 (void)*(char*)f;
211#endif
212
213 return f;
214}
215
216/* FUNCTION: fclose */
217
218#ifndef __CPROVER_STDIO_H_INCLUDED
219#include <stdio.h>
220#define __CPROVER_STDIO_H_INCLUDED
221#endif
222
223#ifndef __CPROVER_STDLIB_H_INCLUDED
224#include <stdlib.h>
225#define __CPROVER_STDLIB_H_INCLUDED
226#endif
227
228int __VERIFIER_nondet_int(void);
229
230 int fclose(FILE *stream)
231{
233#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
234 __CPROVER_assert(__CPROVER_get_must(stream, "open"),
235 "fclose file must be open");
236 __CPROVER_clear_must(stream, "open");
237 __CPROVER_set_must(stream, "closed");
238#endif
239 int return_value=__VERIFIER_nondet_int();
240 free(stream);
241 return return_value;
242}
243
244/* FUNCTION: fdopen */
245
246#ifndef __CPROVER_STDIO_H_INCLUDED
247#include <stdio.h>
248#define __CPROVER_STDIO_H_INCLUDED
249#endif
250
251#ifndef __CPROVER_STDLIB_H_INCLUDED
252#include <stdlib.h>
253#define __CPROVER_STDLIB_H_INCLUDED
254#endif
255
256 FILE *fdopen(int handle, const char *mode)
257{
259 (void)handle;
260 (void)*mode;
261#ifdef __CPROVER_STRING_ABSTRACTION
263 "fdopen zero-termination of 2nd argument");
264#endif
265
266#if !defined(__linux__) || defined(__GLIBC__)
267 FILE *f=malloc(sizeof(FILE));
268#else
269 // libraries need to expose the definition of FILE; this is the
270 // case for musl
271 FILE *f=malloc(sizeof(int));
272#endif
273
274 return f;
275}
276
277/* FUNCTION: _fdopen */
278
279// This is for Apple; we cannot fall back to fdopen as we need
280// header files to have a definition of FILE available; the same
281// header files rename fdopen to _fdopen and would thus yield
282// unbounded recursion.
283
284#ifndef __CPROVER_STDIO_H_INCLUDED
285#include <stdio.h>
286#define __CPROVER_STDIO_H_INCLUDED
287#endif
288
289#ifndef __CPROVER_STDLIB_H_INCLUDED
290#include <stdlib.h>
291#define __CPROVER_STDLIB_H_INCLUDED
292#endif
293
294#ifdef __APPLE__
295FILE *_fdopen(int handle, const char *mode)
296{
297 __CPROVER_HIDE:;
298 (void)handle;
299 (void)*mode;
300#ifdef __CPROVER_STRING_ABSTRACTION
301 __CPROVER_assert(__CPROVER_is_zero_string(mode),
302 "fdopen zero-termination of 2nd argument");
303#endif
304
305 FILE *f=malloc(sizeof(FILE));
306
307 return f;
308}
309#endif
310
311/* FUNCTION: fgets */
312
313#ifndef __CPROVER_STDIO_H_INCLUDED
314#include <stdio.h>
315#define __CPROVER_STDIO_H_INCLUDED
316#endif
317
318__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
319int __VERIFIER_nondet_int(void);
320
321 char *fgets(char *str, int size, FILE *stream)
322{
325
326 (void)size;
327 if(stream != stdin)
328 {
329#if !defined(__linux__) || defined(__GLIBC__)
330 (void)*stream;
331#else
332 (void)*(char *)stream;
333#endif
334 }
335
336#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
337 __CPROVER_assert(__CPROVER_get_must(stream, "open"),
338 "fgets file must be open");
339#endif
340
341#ifdef __CPROVER_STRING_ABSTRACTION
342 int resulting_size;
343 __CPROVER_assert(__CPROVER_buffer_size(str)>=size, "buffer-overflow in fgets");
344 if(size>0)
345 {
347 __CPROVER_is_zero_string(str)=!error;
349 }
350#else
351 if(size>0)
352 {
354 __CPROVER_assume(str_length >= 0 && str_length < size);
355 __CPROVER_precondition(__CPROVER_w_ok(str, size), "fgets buffer writable");
358 if(!error)
359 str[str_length]='0円';
360 }
361#endif
362
363 return error?0:str;
364}
365
366/* FUNCTION: __fgets_chk */
367
368#ifndef __CPROVER_STDIO_H_INCLUDED
369# include <stdio.h>
370# define __CPROVER_STDIO_H_INCLUDED
371#endif
372
373__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
374int __VERIFIER_nondet_int(void);
375
376 char *__fgets_chk(char *str, __CPROVER_size_t bufsize, int size, FILE *stream)
377{
379 (void)bufsize;
381
382 (void)size;
383 if(stream != stdin)
384 {
385#if !defined(__linux__) || defined(__GLIBC__)
386 (void)*stream;
387#else
388 (void)*(char *)stream;
389#endif
390 }
391
392#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
394 __CPROVER_get_must(stream, "open"), "fgets file must be open");
395#endif
396
397#ifdef __CPROVER_STRING_ABSTRACTION
398 int resulting_size;
400 __CPROVER_buffer_size(str) >= size, "buffer-overflow in fgets");
401 if(size > 0)
402 {
404 __CPROVER_is_zero_string(str) = !error;
406 }
407#else
408 if(size > 0)
409 {
411 __CPROVER_assume(str_length >= 0 && str_length < size);
412 __CPROVER_precondition(__CPROVER_w_ok(str, size), "fgets buffer writable");
415 if(!error)
416 str[str_length] = '0円';
417 }
418#endif
419
420 return error ? 0 : str;
421}
422
423/* FUNCTION: fread */
424
425#ifndef __CPROVER_STDIO_H_INCLUDED
426#include <stdio.h>
427#define __CPROVER_STDIO_H_INCLUDED
428#endif
429
430 char __VERIFIER_nondet_char(void);
431 size_t __VERIFIER_nondet_size_t(void);
432
433 size_t fread(void *ptr, size_t size, size_t nitems, FILE *stream)
434{
437 size_t upper_bound = nitems * size;
438 __CPROVER_assume(bytes_read <= upper_bound);
439
440 if(stream != stdin)
441 {
442#if !defined(__linux__) || defined(__GLIBC__)
443 (void)*stream;
444#else
445 (void)*(char *)stream;
446#endif
447 }
448
449#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
450 __CPROVER_assert(__CPROVER_get_must(stream, "open"),
451 "fread file must be open");
452#endif
453
454 for(size_t i = 0; i < bytes_read && i < upper_bound; i++)
455 {
456 ((char *)ptr)[i] = __VERIFIER_nondet_char();
457 }
458
459 return bytes_read / size;
460}
461
462/* FUNCTION: __fread_chk */
463
464#ifndef __CPROVER_STDIO_H_INCLUDED
465# include <stdio.h>
466# define __CPROVER_STDIO_H_INCLUDED
467#endif
468
469char __VERIFIER_nondet_char(void);
470size_t __VERIFIER_nondet_size_t(void);
471
472size_t
473 __fread_chk(void *ptr, size_t ptrlen, size_t size, size_t nitems, FILE *stream)
474{
477 size_t upper_bound = nitems * size;
478 __CPROVER_assume(bytes_read <= upper_bound);
479
480 if(stream != stdin)
481 {
482#if !defined(__linux__) || defined(__GLIBC__)
483 (void)*stream;
484#else
485 (void)*(char *)stream;
486#endif
487 }
488
489#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
491 __CPROVER_get_must(stream, "open"), "fread file must be open");
492#endif
493
494 for(size_t i = 0; i < bytes_read && i < upper_bound && i < ptrlen; i++)
495 {
496 ((char *)ptr)[i] = __VERIFIER_nondet_char();
497 }
498
499 return bytes_read / size;
500}
501
502/* FUNCTION: feof */
503
504#ifndef __CPROVER_STDIO_H_INCLUDED
505#include <stdio.h>
506#define __CPROVER_STDIO_H_INCLUDED
507#endif
508
509int __VERIFIER_nondet_int(void);
510
511 int feof(FILE *stream)
512{
513 // just return nondet
515 int return_value=__VERIFIER_nondet_int();
516
517 if(stream != stdin)
518 {
519#if !defined(__linux__) || defined(__GLIBC__)
520 (void)*stream;
521#else
522 (void)*(char *)stream;
523#endif
524 }
525
526#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
527 __CPROVER_assert(__CPROVER_get_must(stream, "open"),
528 "feof file must be open");
529#endif
530
531 return return_value;
532}
533
534/* FUNCTION: ferror */
535
536#ifndef __CPROVER_STDIO_H_INCLUDED
537#include <stdio.h>
538#define __CPROVER_STDIO_H_INCLUDED
539#endif
540
541int __VERIFIER_nondet_int(void);
542
543 int ferror(FILE *stream)
544{
545 // just return nondet
547 int return_value=__VERIFIER_nondet_int();
548
549 if(stream != stdin)
550 {
551#if !defined(__linux__) || defined(__GLIBC__)
552 (void)*stream;
553#else
554 (void)*(char *)stream;
555#endif
556 }
557
558#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
559 __CPROVER_assert(__CPROVER_get_must(stream, "open"),
560 "feof file must be open");
561#endif
562
563 return return_value;
564}
565
566/* FUNCTION: fileno */
567
568#ifndef __CPROVER_STDIO_H_INCLUDED
569#include <stdio.h>
570#define __CPROVER_STDIO_H_INCLUDED
571#endif
572
573int __VERIFIER_nondet_int(void);
574
575 int fileno(FILE *stream)
576{
578 if(stream == stdin)
579 return 0;
580 else if(stream == stdout)
581 return 1;
582 else if(stream == stderr)
583 return 2;
584
585 int return_value=__VERIFIER_nondet_int();
586 __CPROVER_assume(return_value >= -1);
587
588#if !defined(__linux__) || defined(__GLIBC__)
589 (void)*stream;
590#else
591 (void)*(char*)stream;
592#endif
593
594#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
595 __CPROVER_assert(__CPROVER_get_must(stream, "open"),
596 "fileno file must be open");
597#endif
598
599 return return_value;
600}
601
602/* FUNCTION: fputs */
603
604#ifndef __CPROVER_STDIO_H_INCLUDED
605#include <stdio.h>
606#define __CPROVER_STDIO_H_INCLUDED
607#endif
608
609int __VERIFIER_nondet_int(void);
610
611 int fputs(const char *s, FILE *stream)
612{
613 // just return nondet
615 int return_value=__VERIFIER_nondet_int();
616#ifdef __CPROVER_STRING_ABSTRACTION
617 __CPROVER_assert(__CPROVER_is_zero_string(s), "fputs zero-termination of 1st argument");
618#endif
619 (void)*s;
620
621 if(stream != stdout && stream != stderr)
622 {
623#if !defined(__linux__) || defined(__GLIBC__)
624 (void)*stream;
625#else
626 (void)*(char *)stream;
627#endif
628 }
629
630#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
631 __CPROVER_assert(__CPROVER_get_must(stream, "open"),
632 "fputs file must be open");
633#endif
634
635 return return_value;
636}
637
638/* FUNCTION: fflush */
639
640#ifndef __CPROVER_STDIO_H_INCLUDED
641#include <stdio.h>
642#define __CPROVER_STDIO_H_INCLUDED
643#endif
644
645int __VERIFIER_nondet_int(void);
646
647 int fflush(FILE *stream)
648{
649 // just return nondet
651 int return_value=__VERIFIER_nondet_int();
652 (void)stream;
653
654#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
655 if(stream)
656 __CPROVER_assert(__CPROVER_get_must(stream, "open"),
657 "fflush file must be open");
658#endif
659
660 return return_value;
661}
662
663/* FUNCTION: fpurge */
664
665#ifndef __CPROVER_STDIO_H_INCLUDED
666#include <stdio.h>
667#define __CPROVER_STDIO_H_INCLUDED
668#endif
669
670int __VERIFIER_nondet_int(void);
671
672 int fpurge(FILE *stream)
673{
674 // just return nondet
676 int return_value=__VERIFIER_nondet_int();
677
678 if(stream != stdin && stream != stdout && stream != stderr)
679 {
680#if !defined(__linux__) || defined(__GLIBC__)
681 (void)*stream;
682#else
683 (void)*(char *)stream;
684#endif
685 }
686
687#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
688 __CPROVER_assert(__CPROVER_get_must(stream, "open"),
689 "fpurge file must be open");
690#endif
691
692 return return_value;
693}
694
695/* FUNCTION: fgetc */
696
697#ifndef __CPROVER_STDIO_H_INCLUDED
698#include <stdio.h>
699#define __CPROVER_STDIO_H_INCLUDED
700#endif
701
702int __VERIFIER_nondet_int(void);
703
704 int fgetc(FILE *stream)
705{
707 int return_value=__VERIFIER_nondet_int();
708
709 if(stream != stdin)
710 {
711#if !defined(__linux__) || defined(__GLIBC__)
712 (void)*stream;
713#else
714 (void)*(char *)stream;
715#endif
716 }
717
718 // it's a byte or EOF (-1)
719 __CPROVER_assume(return_value>=-1 && return_value<=255);
720
721 __CPROVER_input("fgetc", return_value);
722
723#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
724 __CPROVER_assert(__CPROVER_get_must(stream, "open"),
725 "fgetc file must be open");
726#endif
727
728 return return_value;
729}
730
731/* FUNCTION: getc */
732
733#ifndef __CPROVER_STDIO_H_INCLUDED
734#include <stdio.h>
735#define __CPROVER_STDIO_H_INCLUDED
736#endif
737
738int __VERIFIER_nondet_int(void);
739
740 int getc(FILE *stream)
741{
743 int return_value=__VERIFIER_nondet_int();
744
745 if(stream != stdin)
746 {
747#if !defined(__linux__) || defined(__GLIBC__)
748 (void)*stream;
749#else
750 (void)*(char *)stream;
751#endif
752 }
753
754#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
755 __CPROVER_assert(__CPROVER_get_must(stream, "open"),
756 "getc file must be open");
757#endif
758
759 // It's a byte or EOF, which we fix to -1.
760 __CPROVER_assume(return_value>=-1 && return_value<=255);
761
762 __CPROVER_input("getc", return_value);
763
764 return return_value;
765}
766
767/* FUNCTION: getchar */
768
769#ifndef __CPROVER_STDIO_H_INCLUDED
770#include <stdio.h>
771#define __CPROVER_STDIO_H_INCLUDED
772#endif
773
774int __VERIFIER_nondet_int(void);
775
776 int getchar(void)
777{
779 int return_value=__VERIFIER_nondet_int();
780 // it's a byte or EOF
781 __CPROVER_assume(return_value>=-1 && return_value<=255);
782 __CPROVER_input("getchar", return_value);
783 return return_value;
784}
785
786/* FUNCTION: getw */
787
788#ifndef __CPROVER_STDIO_H_INCLUDED
789#include <stdio.h>
790#define __CPROVER_STDIO_H_INCLUDED
791#endif
792
793int __VERIFIER_nondet_int(void);
794
795 int getw(FILE *stream)
796{
798 int return_value=__VERIFIER_nondet_int();
799
800 if(stream != stdin)
801 {
802#if !defined(__linux__) || defined(__GLIBC__)
803 (void)*stream;
804#else
805 (void)*(char *)stream;
806#endif
807 }
808
809#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
810 __CPROVER_assert(__CPROVER_get_must(stream, "open"),
811 "getw file must be open");
812#endif
813
814 __CPROVER_input("getw", return_value);
815
816 // it's any int, no restriction
817 return return_value;
818}
819
820/* FUNCTION: fseek */
821
822#ifndef __CPROVER_STDIO_H_INCLUDED
823#include <stdio.h>
824#define __CPROVER_STDIO_H_INCLUDED
825#endif
826
827int __VERIFIER_nondet_int(void);
828
829 int fseek(FILE *stream, long offset, int whence)
830{
832 int return_value=__VERIFIER_nondet_int();
833
834#if !defined(__linux__) || defined(__GLIBC__)
835 (void)*stream;
836#else
837 (void)*(char*)stream;
838#endif
839 (void)offset;
840 (void)whence;
841
842#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
843 __CPROVER_assert(__CPROVER_get_must(stream, "open"),
844 "fseek file must be open");
845#endif
846
847 return return_value;
848}
849
850/* FUNCTION: ftell */
851
852#ifndef __CPROVER_STDIO_H_INCLUDED
853#include <stdio.h>
854#define __CPROVER_STDIO_H_INCLUDED
855#endif
856
857 long __VERIFIER_nondet_long(void);
858
859 long ftell(FILE *stream)
860{
862 long return_value=__VERIFIER_nondet_long();
863
864#if !defined(__linux__) || defined(__GLIBC__)
865 (void)*stream;
866#else
867 (void)*(char*)stream;
868#endif
869
870#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
871 __CPROVER_assert(__CPROVER_get_must(stream, "open"),
872 "ftell file must be open");
873#endif
874
875 return return_value;
876}
877
878/* FUNCTION: rewind */
879
880#ifndef __CPROVER_STDIO_H_INCLUDED
881#include <stdio.h>
882#define __CPROVER_STDIO_H_INCLUDED
883#endif
884
885 void rewind(FILE *stream)
886{
888
889#if !defined(__linux__) || defined(__GLIBC__)
890 (void)*stream;
891#else
892 (void)*(char*)stream;
893#endif
894
895#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
896 __CPROVER_assert(__CPROVER_get_must(stream, "open"),
897 "rewind file must be open");
898#endif
899}
900
901/* FUNCTION: fwrite */
902
903#ifndef __CPROVER_STDIO_H_INCLUDED
904#include <stdio.h>
905#define __CPROVER_STDIO_H_INCLUDED
906#endif
907
908size_t __VERIFIER_nondet_size_t(void);
909
910 size_t fwrite(
911 const void *ptr,
912 size_t size,
913 size_t nitems,
914 FILE *stream)
915{
917 (void)*(char*)ptr;
918 (void)size;
919
920 if(stream != stdout && stream != stderr)
921 {
922#if !defined(__linux__) || defined(__GLIBC__)
923 (void)*stream;
924#else
925 (void)*(char *)stream;
926#endif
927 }
928
929#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
930 __CPROVER_assert(__CPROVER_get_must(stream, "open"),
931 "fwrite file must be open");
932#endif
933
936 return nwrite;
937}
938
939/* FUNCTION: perror */
940
941#ifndef __CPROVER_STDIO_H_INCLUDED
942#include <stdio.h>
943#define __CPROVER_STDIO_H_INCLUDED
944#endif
945
946 void perror(const char *s)
947{
949 if(s!=0)
950 {
951 #ifdef __CPROVER_STRING_ABSTRACTION
952 __CPROVER_assert(__CPROVER_is_zero_string(s), "perror zero-termination");
953 #endif
954 // should go to stderr
955 if(s[0]!=0)
956 __CPROVER_printf("%s: ", s);
957 }
958
959 // TODO: print errno error
960}
961
962/* FUNCTION: fscanf */
963
964#if !defined(__USE_ISOC99) || !defined(__REDIRECT)
965
966# ifndef __CPROVER_STDIO_H_INCLUDED
967# include <stdio.h>
968# define __CPROVER_STDIO_H_INCLUDED
969# endif
970
971# ifndef __CPROVER_STDARG_H_INCLUDED
972# include <stdarg.h>
973 # define __CPROVER_STDARG_H_INCLUDED
974# endif
975
976 int fscanf(FILE *restrict stream, const char *restrict format, ...)
977{
979 va_list list;
980 va_start(list, format);
981 int result=vfscanf(stream, format, list);
982 va_end(list);
983 return result;
984}
985
986#endif
987
988/* FUNCTION: __isoc99_fscanf */
989
990#ifndef __CPROVER_STDIO_H_INCLUDED
991# include <stdio.h>
992# define __CPROVER_STDIO_H_INCLUDED
993#endif
994
995#ifndef __CPROVER_STDARG_H_INCLUDED
996# include <stdarg.h>
997# define __CPROVER_STDARG_H_INCLUDED
998#endif
999
1000 int __isoc99_fscanf(FILE *restrict stream, const char *restrict format, ...)
1001{
1003 va_list list;
1004 va_start(list, format);
1005 int result = vfscanf(stream, format, list);
1006 va_end(list);
1007 return result;
1008}
1009
1010/* FUNCTION: scanf */
1011
1012#if !defined(__USE_ISOC99) || !defined(__REDIRECT)
1013
1014# ifndef __CPROVER_STDIO_H_INCLUDED
1015# include <stdio.h>
1016# define __CPROVER_STDIO_H_INCLUDED
1017# endif
1018
1019# ifndef __CPROVER_STDARG_H_INCLUDED
1020# include <stdarg.h>
1021# define __CPROVER_STDARG_H_INCLUDED
1022# endif
1023
1024 int scanf(const char *restrict format, ...)
1025{
1027 va_list list;
1028 va_start(list, format);
1029 int result=vfscanf(stdin, format, list);
1030 va_end(list);
1031 return result;
1032}
1033
1034#endif
1035
1036/* FUNCTION: __isoc99_scanf */
1037
1038#ifndef __CPROVER_STDIO_H_INCLUDED
1039# include <stdio.h>
1040# define __CPROVER_STDIO_H_INCLUDED
1041#endif
1042
1043#ifndef __CPROVER_STDARG_H_INCLUDED
1044# include <stdarg.h>
1045# define __CPROVER_STDARG_H_INCLUDED
1046#endif
1047
1048 int __isoc99_scanf(const char *restrict format, ...)
1049{
1051 va_list list;
1052 va_start(list, format);
1053 int result = vfscanf(stdin, format, list);
1054 va_end(list);
1055 return result;
1056}
1057
1058/* FUNCTION: sscanf */
1059
1060#if !defined(__USE_ISOC99) || !defined(__REDIRECT)
1061
1062# ifndef __CPROVER_STDIO_H_INCLUDED
1063# include <stdio.h>
1064# define __CPROVER_STDIO_H_INCLUDED
1065# endif
1066
1067# ifndef __CPROVER_STDARG_H_INCLUDED
1068# include <stdarg.h>
1069# define __CPROVER_STDARG_H_INCLUDED
1070# endif
1071
1072 int sscanf(const char *restrict s, const char *restrict format, ...)
1073{
1075 va_list list;
1076 va_start(list, format);
1077 int result=vsscanf(s, format, list);
1078 va_end(list);
1079 return result;
1080}
1081
1082#endif
1083
1084/* FUNCTION: __isoc99_sscanf */
1085
1086#ifndef __CPROVER_STDIO_H_INCLUDED
1087# include <stdio.h>
1088# define __CPROVER_STDIO_H_INCLUDED
1089#endif
1090
1091#ifndef __CPROVER_STDARG_H_INCLUDED
1092# include <stdarg.h>
1093# define __CPROVER_STDARG_H_INCLUDED
1094#endif
1095
1096 int __isoc99_sscanf(const char *restrict s, const char *restrict format, ...)
1097{
1099 va_list list;
1100 va_start(list, format);
1101 int result = vsscanf(s, format, list);
1102 va_end(list);
1103 return result;
1104}
1105
1106/* FUNCTION: vfscanf */
1107
1108#if !defined(__USE_ISOC99) || !defined(__REDIRECT)
1109
1110# ifndef __CPROVER_STDIO_H_INCLUDED
1111# include <stdio.h>
1112# define __CPROVER_STDIO_H_INCLUDED
1113# endif
1114
1115# ifndef __CPROVER_STDARG_H_INCLUDED
1116# include <stdarg.h>
1117# define __CPROVER_STDARG_H_INCLUDED
1118# endif
1119
1120int __VERIFIER_nondet_int(void);
1121
1122 int vfscanf(FILE *restrict stream, const char *restrict format, va_list arg)
1123{
1125 int result=__VERIFIER_nondet_int();
1126
1127 if(stream != stdin)
1128 {
1129#if !defined(__linux__) || defined(__GLIBC__)
1130 (void)*stream;
1131#else
1132 (void)*(char *)stream;
1133#endif
1134 }
1135
1136 (void)*format;
1137# if(defined(__aarch64__) || defined(_M_ARM64)) && !defined(__APPLE__)
1138 while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(arg.__stack) <
1139 __CPROVER_OBJECT_SIZE(arg.__stack))
1140 {
1141 void *a = va_arg(arg, void *);
1143 }
1144# else
1147 {
1148 void *a = va_arg(arg, void *);
1150 }
1151# endif
1152
1153# ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
1154 __CPROVER_assert(__CPROVER_get_must(stream, "open"),
1155 "vfscanf file must be open");
1156#endif
1157
1158 return result;
1159}
1160
1161#endif
1162
1163/* FUNCTION: __isoc99_vfscanf */
1164
1165#ifndef __CPROVER_STDIO_H_INCLUDED
1166# include <stdio.h>
1167# define __CPROVER_STDIO_H_INCLUDED
1168#endif
1169
1170#ifndef __CPROVER_STDARG_H_INCLUDED
1171# include <stdarg.h>
1172# define __CPROVER_STDARG_H_INCLUDED
1173#endif
1174
1175int __VERIFIER_nondet_int(void);
1176
1178 FILE *restrict stream,
1179 const char *restrict format,
1180 va_list arg)
1181{
1183 int result = __VERIFIER_nondet_int();
1184
1185 if(stream != stdin)
1186 {
1187#if !defined(__linux__) || defined(__GLIBC__)
1188 (void)*stream;
1189#else
1190 (void)*(char *)stream;
1191#endif
1192 }
1193
1194 (void)*format;
1195#if(defined(__aarch64__) || defined(_M_ARM64)) && !defined(__APPLE__)
1196 while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(arg.__stack) <
1197 __CPROVER_OBJECT_SIZE(arg.__stack))
1198 {
1199 void *a = va_arg(arg, void *);
1201 }
1202#else
1205 {
1206 void *a = va_arg(arg, void *);
1208 }
1209#endif
1210
1211#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
1213 __CPROVER_get_must(stream, "open"), "vfscanf file must be open");
1214#endif
1215
1216 return result;
1217}
1218
1219/* FUNCTION: __stdio_common_vfscanf */
1220
1221#ifdef _WIN32
1222
1223# ifndef __CPROVER_STDIO_H_INCLUDED
1224# include <stdio.h>
1225# define __CPROVER_STDIO_H_INCLUDED
1226# endif
1227
1228# ifndef __CPROVER_STDARG_H_INCLUDED
1229# include <stdarg.h>
1230# define __CPROVER_STDARG_H_INCLUDED
1231# endif
1232
1233int __VERIFIER_nondet_int(void);
1234
1235int __stdio_common_vfscanf(
1236 unsigned __int64 options,
1237 FILE *stream,
1238 char const *format,
1239 _locale_t locale,
1240 va_list args)
1241{
1242 (void)options;
1243 (void)locale;
1244
1245 int result = __VERIFIER_nondet_int();
1246
1247 if(stream != stdin)
1248 {
1249 (void)*(char *)stream;
1250 }
1251
1252 (void)*format;
1253# if(defined(__aarch64__) || defined(_M_ARM64)) && !defined(__APPLE__)
1254 while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(args.__stack) <
1255 __CPROVER_OBJECT_SIZE(args.__stack))
1256 {
1257 void *a = va_arg(args, void *);
1258 __CPROVER_havoc_object(a);
1259 }
1260# else
1261 while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(args) <
1262 __CPROVER_OBJECT_SIZE(args))
1263 {
1264 void *a = va_arg(args, void *);
1265 __CPROVER_havoc_object(a);
1266 }
1267# endif
1268
1269# ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
1270 __CPROVER_assert(
1271 __CPROVER_get_must(stream, "open"), "vfscanf file must be open");
1272# endif
1273
1274 return result;
1275}
1276
1277#endif
1278
1279/* FUNCTION: vscanf */
1280
1281#if !defined(__USE_ISOC99) || !defined(__REDIRECT)
1282
1283# ifndef __CPROVER_STDIO_H_INCLUDED
1284# include <stdio.h>
1285# define __CPROVER_STDIO_H_INCLUDED
1286# endif
1287
1288# ifndef __CPROVER_STDARG_H_INCLUDED
1289# include <stdarg.h>
1290# define __CPROVER_STDARG_H_INCLUDED
1291# endif
1292
1293 int vscanf(const char *restrict format, va_list arg)
1294{
1296 return vfscanf(stdin, format, arg);
1297}
1298
1299#endif
1300
1301/* FUNCTION: __isoc99_vscanf */
1302
1303#ifndef __CPROVER_STDIO_H_INCLUDED
1304# include <stdio.h>
1305# define __CPROVER_STDIO_H_INCLUDED
1306#endif
1307
1308#ifndef __CPROVER_STDARG_H_INCLUDED
1309# include <stdarg.h>
1310# define __CPROVER_STDARG_H_INCLUDED
1311#endif
1312
1314{
1316 return vfscanf(stdin, format, arg);
1317}
1318
1319/* FUNCTION: vsscanf */
1320
1321#if !defined(__USE_ISOC99) || !defined(__REDIRECT)
1322
1323# ifndef __CPROVER_STDIO_H_INCLUDED
1324# include <stdio.h>
1325# define __CPROVER_STDIO_H_INCLUDED
1326# endif
1327
1328# ifndef __CPROVER_STDARG_H_INCLUDED
1329# include <stdarg.h>
1330# define __CPROVER_STDARG_H_INCLUDED
1331# endif
1332
1333int __VERIFIER_nondet_int(void);
1334
1335 int vsscanf(const char *restrict s, const char *restrict format, va_list arg)
1336{
1338 int result = __VERIFIER_nondet_int();
1339 (void)*s;
1340 (void)*format;
1341# if(defined(__aarch64__) || defined(_M_ARM64)) && !defined(__APPLE__)
1342 while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(arg.__stack) <
1343 __CPROVER_OBJECT_SIZE(arg.__stack))
1344 {
1345 void *a = va_arg(arg, void *);
1347 }
1348# else
1351 {
1352 void *a = va_arg(arg, void *);
1354 }
1355# endif
1356
1357 return result;
1358}
1359
1360#endif
1361
1362/* FUNCTION: __isoc99_vsscanf */
1363
1364#ifndef __CPROVER_STDIO_H_INCLUDED
1365# include <stdio.h>
1366# define __CPROVER_STDIO_H_INCLUDED
1367#endif
1368
1369#ifndef __CPROVER_STDARG_H_INCLUDED
1370# include <stdarg.h>
1371# define __CPROVER_STDARG_H_INCLUDED
1372#endif
1373
1374int __VERIFIER_nondet_int(void);
1375
1377 const char *restrict s,
1378 const char *restrict format,
1379 va_list arg)
1380{
1382 int result = __VERIFIER_nondet_int();
1383 (void)*s;
1384 (void)*format;
1385#if(defined(__aarch64__) || defined(_M_ARM64)) && !defined(__APPLE__)
1386 while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(arg.__stack) <
1387 __CPROVER_OBJECT_SIZE(arg.__stack))
1388 {
1389 void *a = va_arg(arg, void *);
1391 }
1392#else
1395 {
1396 void *a = va_arg(arg, void *);
1398 }
1399#endif
1400
1401 return result;
1402}
1403
1404/* FUNCTION: __stdio_common_vsscanf */
1405
1406#ifdef _WIN32
1407
1408# ifndef __CPROVER_STDIO_H_INCLUDED
1409# include <stdio.h>
1410# define __CPROVER_STDIO_H_INCLUDED
1411# endif
1412
1413# ifndef __CPROVER_STDARG_H_INCLUDED
1414# include <stdarg.h>
1415# define __CPROVER_STDARG_H_INCLUDED
1416# endif
1417
1418int __VERIFIER_nondet_int(void);
1419
1420int __stdio_common_vsscanf(
1421 unsigned __int64 options,
1422 char const *s,
1423 size_t buffer_count,
1424 char const *format,
1425 _locale_t locale,
1426 va_list args)
1427{
1428 (void)options;
1429 (void)locale;
1430
1431 int result = __VERIFIER_nondet_int();
1432
1433 (void)*s;
1434 (void)*format;
1435# if(defined(__aarch64__) || defined(_M_ARM64)) && !defined(__APPLE__)
1436 while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(args.__stack) <
1437 __CPROVER_OBJECT_SIZE(args.__stack))
1438 {
1439 void *a = va_arg(args, void *);
1440 __CPROVER_havoc_object(a);
1441 }
1442# else
1443 while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(args) <
1444 __CPROVER_OBJECT_SIZE(args))
1445 {
1446 void *a = va_arg(args, void *);
1447 __CPROVER_havoc_object(a);
1448 }
1449# endif
1450
1451 return result;
1452}
1453
1454#endif
1455
1456/* FUNCTION: printf */
1457
1458#ifndef __CPROVER_STDIO_H_INCLUDED
1459# include <stdio.h>
1460# define __CPROVER_STDIO_H_INCLUDED
1461#endif
1462
1463#ifndef __CPROVER_STDARG_H_INCLUDED
1464# include <stdarg.h>
1465# define __CPROVER_STDARG_H_INCLUDED
1466#endif
1467
1468int __VERIFIER_nondet_int(void);
1469
1470 int printf(const char *format, ...)
1471{
1473 int result = __VERIFIER_nondet_int();
1474 va_list list;
1475 va_start(list, format);
1476 __CPROVER_printf(format, list);
1477 va_end(list);
1478 return result;
1479}
1480
1481/* FUNCTION: __printf_chk */
1482
1483#ifndef __CPROVER_STDIO_H_INCLUDED
1484# include <stdio.h>
1485# define __CPROVER_STDIO_H_INCLUDED
1486#endif
1487
1488#ifndef __CPROVER_STDARG_H_INCLUDED
1489# include <stdarg.h>
1490# define __CPROVER_STDARG_H_INCLUDED
1491#endif
1492
1493int __VERIFIER_nondet_int(void);
1494
1495 int __printf_chk(int flag, const char *format, ...)
1496{
1498 (void)flag;
1499 int result = __VERIFIER_nondet_int();
1500 va_list list;
1501 va_start(list, format);
1502 __CPROVER_printf(format, list);
1503 va_end(list);
1504 return result;
1505}
1506
1507/* FUNCTION: fprintf */
1508
1509#ifndef __CPROVER_STDIO_H_INCLUDED
1510#include <stdio.h>
1511#define __CPROVER_STDIO_H_INCLUDED
1512#endif
1513
1514#ifndef __CPROVER_STDARG_H_INCLUDED
1515#include <stdarg.h>
1516#define __CPROVER_STDARG_H_INCLUDED
1517#endif
1518
1519 int fprintf(FILE *stream, const char *restrict format, ...)
1520{
1522 va_list list;
1523 va_start(list, format);
1524 int result=vfprintf(stream, format, list);
1525 va_end(list);
1526 return result;
1527}
1528
1529/* FUNCTION: __fprintf_chk */
1530
1531#ifndef __CPROVER_STDIO_H_INCLUDED
1532# include <stdio.h>
1533# define __CPROVER_STDIO_H_INCLUDED
1534#endif
1535
1536#ifndef __CPROVER_STDARG_H_INCLUDED
1537# include <stdarg.h>
1538# define __CPROVER_STDARG_H_INCLUDED
1539#endif
1540
1541 int __fprintf_chk(FILE *stream, int flag, const char *restrict format, ...)
1542{
1544 (void)flag;
1545 va_list list;
1546 va_start(list, format);
1547 int result = vfprintf(stream, format, list);
1548 va_end(list);
1549 return result;
1550}
1551
1552/* FUNCTION: vfprintf */
1553
1554#ifndef __CPROVER_STDIO_H_INCLUDED
1555#include <stdio.h>
1556#define __CPROVER_STDIO_H_INCLUDED
1557#endif
1558
1559#ifndef __CPROVER_STDARG_H_INCLUDED
1560#include <stdarg.h>
1561#define __CPROVER_STDARG_H_INCLUDED
1562#endif
1563
1564int __VERIFIER_nondet_int(void);
1565
1566 int vfprintf(FILE *stream, const char *restrict format, va_list arg)
1567{
1569
1570 int result=__VERIFIER_nondet_int();
1571
1572 if(stream != stdout && stream != stderr)
1573 {
1574#if !defined(__linux__) || defined(__GLIBC__)
1575 (void)*stream;
1576#else
1577 (void)*(char *)stream;
1578#endif
1579 }
1580
1581 (void)*format;
1582 (void)arg;
1583
1584#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
1585 __CPROVER_assert(__CPROVER_get_must(stream, "open"),
1586 "vfprintf file must be open");
1587#endif
1588
1589 return result;
1590}
1591
1592/* FUNCTION: __vfprintf_chk */
1593
1594#ifndef __CPROVER_STDIO_H_INCLUDED
1595# include <stdio.h>
1596# define __CPROVER_STDIO_H_INCLUDED
1597#endif
1598
1599#ifndef __CPROVER_STDARG_H_INCLUDED
1600# include <stdarg.h>
1601# define __CPROVER_STDARG_H_INCLUDED
1602#endif
1603
1604int __VERIFIER_nondet_int(void);
1605
1607 FILE *stream,
1608 int flag,
1609 const char *restrict format,
1610 va_list arg)
1611{
1613 (void)flag;
1614
1615 int result = __VERIFIER_nondet_int();
1616
1617 if(stream != stdout && stream != stderr)
1618 {
1619#if !defined(__linux__) || defined(__GLIBC__)
1620 (void)*stream;
1621#else
1622 (void)*(char *)stream;
1623#endif
1624 }
1625
1626 (void)*format;
1627 (void)arg;
1628
1629#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
1631 __CPROVER_get_must(stream, "open"), "vfprintf file must be open");
1632#endif
1633
1634 return result;
1635}
1636
1637/* FUNCTION: asprintf */
1638
1639#ifndef __CPROVER_STDARG_H_INCLUDED
1640# include <stdarg.h>
1641# define __CPROVER_STDARG_H_INCLUDED
1642#endif
1643
1644// declare here instead of relying on stdio.h as even those platforms that do
1645// have it at all may require _GNU_SOURCE to be set
1646int vasprintf(char **ptr, const char *fmt, va_list ap);
1647
1648 int asprintf(char **ptr, const char *fmt, ...)
1649{
1650 va_list list;
1651 va_start(list, fmt);
1652 int result = vasprintf(ptr, fmt, list);
1653 va_end(list);
1654 return result;
1655}
1656
1657/* FUNCTION: dprintf */
1658
1659#ifndef __CPROVER_STDIO_H_INCLUDED
1660# include <stdio.h>
1661# define __CPROVER_STDIO_H_INCLUDED
1662#endif
1663
1664#ifndef __CPROVER_STDARG_H_INCLUDED
1665# include <stdarg.h>
1666# define __CPROVER_STDARG_H_INCLUDED
1667#endif
1668
1669 int dprintf(int fd, const char *restrict format, ...)
1670{
1672 va_list list;
1673 va_start(list, format);
1674 int result = vdprintf(fd, format, list);
1675 va_end(list);
1676 return result;
1677}
1678
1679/* FUNCTION: vdprintf */
1680
1681#ifndef __CPROVER_STDIO_H_INCLUDED
1682# include <stdio.h>
1683# define __CPROVER_STDIO_H_INCLUDED
1684#endif
1685
1686#ifndef __CPROVER_STDARG_H_INCLUDED
1687# include <stdarg.h>
1688# define __CPROVER_STDARG_H_INCLUDED
1689#endif
1690
1691int __VERIFIER_nondet_int(void);
1692
1693 int vdprintf(int fd, const char *restrict format, va_list arg)
1694{
1696
1697 int result = __VERIFIER_nondet_int();
1698
1699 (void)fd;
1700 (void)*format;
1701 (void)arg;
1702
1703 return result;
1704}
1705
1706/* FUNCTION: vasprintf */
1707
1708#ifndef __CPROVER_STDIO_H_INCLUDED
1709#include <stdio.h>
1710#define __CPROVER_STDIO_H_INCLUDED
1711#endif
1712
1713#ifndef __CPROVER_STDARG_H_INCLUDED
1714#include <stdarg.h>
1715#define __CPROVER_STDARG_H_INCLUDED
1716#endif
1717
1718#ifndef __CPROVER_STDLIB_H_INCLUDED
1719#include <stdlib.h>
1720#define __CPROVER_STDLIB_H_INCLUDED
1721#endif
1722
1723char __VERIFIER_nondet_char(void);
1724int __VERIFIER_nondet_int(void);
1725
1726 int vasprintf(char **ptr, const char *fmt, va_list ap)
1727{
1728 (void)*fmt;
1729 (void)ap;
1730
1732 if(result_buffer_size<=0)
1733 return -1;
1734
1736 if(!*ptr)
1737 return -1;
1738 int i=0;
1739 for( ; i<result_buffer_size; ++i)
1740 {
1742 (*ptr)[i]=c;
1743 if(c=='0円')
1744 break;
1745 }
1746
1748
1749 return i;
1750}
1751
1752/* FUNCTION: snprintf */
1753
1754#ifndef __CPROVER_STDIO_H_INCLUDED
1755# include <stdio.h>
1756# define __CPROVER_STDIO_H_INCLUDED
1757#endif
1758
1759#ifndef __CPROVER_STDARG_H_INCLUDED
1760# include <stdarg.h>
1761# define __CPROVER_STDARG_H_INCLUDED
1762#endif
1763
1764#undef snprintf
1765
1766 int snprintf(char *str, size_t size, const char *fmt, ...)
1767{
1768 va_list list;
1769 va_start(list, fmt);
1770 int result = vsnprintf(str, size, fmt, list);
1771 va_end(list);
1772 return result;
1773}
1774
1775/* FUNCTION: __builtin___snprintf_chk */
1776
1777#ifndef __CPROVER_STDIO_H_INCLUDED
1778# include <stdio.h>
1779# define __CPROVER_STDIO_H_INCLUDED
1780#endif
1781
1782#ifndef __CPROVER_STDARG_H_INCLUDED
1783# include <stdarg.h>
1784# define __CPROVER_STDARG_H_INCLUDED
1785#endif
1786
1787int __builtin___vsnprintf_chk(
1788 char *str,
1789 size_t size,
1790 int flag,
1791 size_t bufsize,
1792 const char *fmt,
1793 va_list ap);
1794
1796 char *str,
1797 size_t size,
1798 int flag,
1799 size_t bufsize,
1800 const char *fmt,
1801 ...)
1802{
1803 va_list list;
1804 va_start(list, fmt);
1805 int result = __builtin___vsnprintf_chk(str, size, flag, bufsize, fmt, list);
1806 va_end(list);
1807 return result;
1808}
1809
1810/* FUNCTION: vsnprintf */
1811
1812#ifndef __CPROVER_STDIO_H_INCLUDED
1813# include <stdio.h>
1814# define __CPROVER_STDIO_H_INCLUDED
1815#endif
1816
1817#ifndef __CPROVER_STDARG_H_INCLUDED
1818# include <stdarg.h>
1819# define __CPROVER_STDARG_H_INCLUDED
1820#endif
1821
1822#undef vsnprintf
1823
1824char __VERIFIER_nondet_char(void);
1825
1826 int vsnprintf(char *str, size_t size, const char *fmt, va_list ap)
1827{
1828 (void)*fmt;
1829
1830#if(defined(__aarch64__) || defined(_M_ARM64)) && !defined(__APPLE__)
1832 __CPROVER_OBJECT_SIZE(ap.__stack))
1833
1834 {
1835 (void)va_arg(ap, int);
1838 "vsnprintf object overlap");
1839 }
1840#else
1843
1844 {
1845 (void)va_arg(ap, int);
1848 "vsnprintf object overlap");
1849 }
1850#endif
1851
1852 size_t i = 0;
1853 for(; i < size; ++i)
1854 {
1855 char c = __VERIFIER_nondet_char();
1856 str[i] = c;
1857 if(c == '0円')
1858 break;
1859 }
1860
1861 return i;
1862}
1863
1864/* FUNCTION: __builtin___vsnprintf_chk */
1865
1866#ifndef __CPROVER_STDIO_H_INCLUDED
1867# include <stdio.h>
1868# define __CPROVER_STDIO_H_INCLUDED
1869#endif
1870
1871#ifndef __CPROVER_STDARG_H_INCLUDED
1872# include <stdarg.h>
1873# define __CPROVER_STDARG_H_INCLUDED
1874#endif
1875
1876char __VERIFIER_nondet_char(void);
1877
1879 char *str,
1880 size_t size,
1881 int flag,
1882 size_t bufsize,
1883 const char *fmt,
1884 va_list ap)
1885{
1886 (void)flag;
1887 (void)bufsize;
1888 (void)*fmt;
1889
1890#if(defined(__aarch64__) || defined(_M_ARM64)) && !defined(__APPLE__)
1892 __CPROVER_OBJECT_SIZE(ap.__stack))
1893
1894 {
1895 (void)va_arg(ap, int);
1898 "vsnprintf object overlap");
1899 }
1900#else
1903
1904 {
1905 (void)va_arg(ap, int);
1908 "vsnprintf object overlap");
1909 }
1910#endif
1911
1912 size_t i = 0;
1913 for(; i < size; ++i)
1914 {
1915 char c = __VERIFIER_nondet_char();
1916 str[i] = c;
1917 if(c == '0円')
1918 break;
1919 }
1920
1921 return i;
1922}
1923
1924/* FUNCTION: __acrt_iob_func */
1925
1926#ifdef _WIN32
1927
1928# ifndef __CPROVER_STDIO_H_INCLUDED
1929# include <stdio.h>
1930# define __CPROVER_STDIO_H_INCLUDED
1931# endif
1932
1933FILE *__acrt_iob_func(unsigned fd)
1934{
1935 static FILE stdin_file;
1936 static FILE stdout_file;
1937 static FILE stderr_file;
1938
1939 switch(fd)
1940 {
1941 case 0:
1942 return &stdin_file;
1943 case 1:
1944 return &stdout_file;
1945 case 2:
1946 return &stderr_file;
1947 default:
1948 return (FILE *)0;
1949 }
1950}
1951
1952#endif
1953
1954/* FUNCTION: __stdio_common_vfprintf */
1955
1956#ifdef _WIN32
1957
1958# ifndef __CPROVER_STDIO_H_INCLUDED
1959# include <stdio.h>
1960# define __CPROVER_STDIO_H_INCLUDED
1961# endif
1962
1963# ifndef __CPROVER_STDARG_H_INCLUDED
1964# include <stdarg.h>
1965# define __CPROVER_STDARG_H_INCLUDED
1966# endif
1967
1968int __stdio_common_vfprintf(
1969 unsigned __int64 options,
1970 FILE *stream,
1971 char const *format,
1972 _locale_t locale,
1973 va_list args)
1974{
1975 (void)options;
1976 (void)locale;
1977
1978 if(stream == __acrt_iob_func(1))
1979 __CPROVER_printf(format, args);
1980 return 0;
1981}
1982
1983#endif
1984
1985/* FUNCTION: __stdio_common_vsprintf */
1986
1987#ifdef _WIN32
1988
1989# ifndef __CPROVER_STDIO_H_INCLUDED
1990# include <stdio.h>
1991# define __CPROVER_STDIO_H_INCLUDED
1992# endif
1993
1994# ifndef __CPROVER_STDARG_H_INCLUDED
1995# include <stdarg.h>
1996# define __CPROVER_STDARG_H_INCLUDED
1997# endif
1998
1999char __VERIFIER_nondet_char(void);
2000
2001int __stdio_common_vsprintf(
2002 unsigned __int64 options,
2003 char *str,
2004 size_t size,
2005 char const *fmt,
2006 _locale_t locale,
2007 va_list args)
2008{
2009 (void)options;
2010 (void)*fmt;
2011 (void)locale;
2012 (void)args;
2013
2014 size_t i = 0;
2015 for(; i < size; ++i)
2016 {
2017 char c = __VERIFIER_nondet_char();
2018 str[i] = c;
2019 if(c == '0円')
2020 break;
2021 }
2022
2023 return i;
2024}
2025
2026#endif
2027
2028/* FUNCTION: __srget */
2029
2030#ifdef __FreeBSD__
2031
2032# ifndef __CPROVER_STDIO_H_INCLUDED
2033# include <stdio.h>
2034# define __CPROVER_STDIO_H_INCLUDED
2035# endif
2036
2037int __VERIFIER_nondet_int(void);
2038
2039int __srget(FILE *stream)
2040{
2041 (void)*stream;
2042
2043 // FreeBSD's implementation returns a character or EOF; __VERIFIER_nondet_int
2044 // will capture all these options
2045 return __VERIFIER_nondet_int();
2046}
2047
2048#endif
2049
2050/* FUNCTION: __swbuf */
2051
2052#ifdef __FreeBSD__
2053
2054# ifndef __CPROVER_STDIO_H_INCLUDED
2055# include <stdio.h>
2056# define __CPROVER_STDIO_H_INCLUDED
2057# endif
2058
2059__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
2060
2061int __swbuf(int c, FILE *stream)
2062{
2063 (void)c;
2064 (void)*stream;
2065
2066 // FreeBSD's implementation returns `c` or or EOF in case writing failed; we
2067 // just non-deterministically choose between these
2068 if(__VERIFIER_nondet___CPROVER_bool())
2069 return EOF;
2070 else
2071 return c;
2072}
2073
2074#endif
__CPROVER_bool __CPROVER_w_ok(const void *,...)
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_printf(const char *format,...)
__CPROVER_size_t __CPROVER_OBJECT_SIZE(const void *)
void __CPROVER_clear_must(const void *, const char *)
void __CPROVER_assert(__CPROVER_bool assertion, const char *description)
void __CPROVER_array_replace(const void *dest, const void *src)
__CPROVER_size_t __CPROVER_POINTER_OFFSET(const void *)
__CPROVER_size_t __CPROVER_POINTER_OBJECT(const void *)
__CPROVER_size_t __CPROVER_zero_string_length(const void *)
__CPROVER_bool __CPROVER_get_must(const void *, const char *)
void __CPROVER_input(const char *id,...)
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_cleanup(const void *, const void *)
void __CPROVER_assume(__CPROVER_bool assumption)
void __CPROVER_havoc_object(void *)
static format_containert< T > format(const T &o)
Definition format.h:37
mini_bddt restrict(const mini_bddt &u, unsigned var, const bool value)
Definition miniBDD.cpp:551
int __VERIFIER_nondet_int(void)
int vscanf(const char *restrict format, va_list arg)
Definition stdio.c:1293
int __isoc99_sscanf(const char *restrict s, const char *restrict format,...)
Definition stdio.c:1096
void fclose_cleanup(void *stream)
int vsnprintf(char *str, size_t size, const char *fmt, va_list ap)
Definition stdio.c:1826
int vasprintf(char **ptr, const char *fmt, va_list ap)
Definition stdio.c:1726
int dprintf(int fd, const char *restrict format,...)
Definition stdio.c:1669
FILE * fdopen(int handle, const char *mode)
Definition stdio.c:256
int __isoc99_vscanf(const char *restrict format, va_list arg)
Definition stdio.c:1313
int scanf(const char *restrict format,...)
Definition stdio.c:1024
int snprintf(char *str, size_t size, const char *fmt,...)
Definition stdio.c:1766
int getchar(void)
Definition stdio.c:776
int __fprintf_chk(FILE *stream, int flag, const char *restrict format,...)
Definition stdio.c:1541
int sscanf(const char *restrict s, const char *restrict format,...)
Definition stdio.c:1072
int asprintf(char **ptr, const char *fmt,...)
Definition stdio.c:1648
size_t fwrite(const void *ptr, size_t size, size_t nitems, FILE *stream)
Definition stdio.c:910
size_t fread(void *ptr, size_t size, size_t nitems, FILE *stream)
Definition stdio.c:433
int ferror(FILE *stream)
Definition stdio.c:543
int __isoc99_fscanf(FILE *restrict stream, const char *restrict format,...)
Definition stdio.c:1000
int __printf_chk(int flag, const char *format,...)
Definition stdio.c:1495
int vfscanf(FILE *restrict stream, const char *restrict format, va_list arg)
Definition stdio.c:1122
int vsscanf(const char *restrict s, const char *restrict format, va_list arg)
Definition stdio.c:1335
char * fgets(char *str, int size, FILE *stream)
Definition stdio.c:321
long ftell(FILE *stream)
Definition stdio.c:859
int __isoc99_vsscanf(const char *restrict s, const char *restrict format, va_list arg)
Definition stdio.c:1376
int __builtin___vsnprintf_chk(char *str, size_t size, int flag, size_t bufsize, const char *fmt, va_list ap)
Definition stdio.c:1878
int fseek(FILE *stream, long offset, int whence)
Definition stdio.c:829
char __VERIFIER_nondet_char(void)
int __builtin___snprintf_chk(char *str, size_t size, int flag, size_t bufsize, const char *fmt,...)
Definition stdio.c:1795
int fputs(const char *s, FILE *stream)
Definition stdio.c:611
int getw(FILE *stream)
Definition stdio.c:795
int fclose(FILE *stream)
Definition stdio.c:230
FILE * fopen(const char *filename, const char *mode)
Definition stdio.c:77
char * __fgets_chk(char *str, __CPROVER_size_t bufsize, int size, FILE *stream)
Definition stdio.c:376
FILE * freopen(const char *filename, const char *mode, FILE *f)
Definition stdio.c:189
int __isoc99_scanf(const char *restrict format,...)
Definition stdio.c:1048
FILE * fopen64(const char *filename, const char *mode)
Definition stdio.c:147
FILE * freopen64(const char *filename, const char *mode, FILE *f)
Definition stdio.c:202
__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void)
int printf(const char *format,...)
Definition stdio.c:1470
size_t __VERIFIER_nondet_size_t(void)
int feof(FILE *stream)
Definition stdio.c:511
void rewind(FILE *stream)
Definition stdio.c:885
int fprintf(FILE *stream, const char *restrict format,...)
Definition stdio.c:1519
int vdprintf(int fd, const char *restrict format, va_list arg)
Definition stdio.c:1693
int __vfprintf_chk(FILE *stream, int flag, const char *restrict format, va_list arg)
Definition stdio.c:1606
int fgetc(FILE *stream)
Definition stdio.c:704
void perror(const char *s)
Definition stdio.c:946
size_t __fread_chk(void *ptr, size_t ptrlen, size_t size, size_t nitems, FILE *stream)
Definition stdio.c:473
int __isoc99_vfscanf(FILE *restrict stream, const char *restrict format, va_list arg)
Definition stdio.c:1177
int puts(const char *s)
Definition stdio.c:39
int getc(FILE *stream)
Definition stdio.c:740
int fflush(FILE *stream)
Definition stdio.c:647
int vfprintf(FILE *stream, const char *restrict format, va_list arg)
Definition stdio.c:1566
int putchar(int c)
Definition stdio.c:21
int fpurge(FILE *stream)
Definition stdio.c:672
int fileno(FILE *stream)
Definition stdio.c:575
long __VERIFIER_nondet_long(void)
int fscanf(FILE *restrict stream, const char *restrict format,...)
Definition stdio.c:976
void * malloc(__CPROVER_size_t malloc_size)
Definition stdlib.c:212
void free(void *ptr)
Definition stdlib.c:317

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