@@ -888,6 +888,28 @@ __CPROVER_HIDE:;
888
888
return result ;
889
889
}
890
890
891
+ /* FUNCTION: __isoc99_scanf */
892
+
893
+ #ifndef __CPROVER_STDIO_H_INCLUDED
894
+ # include <stdio.h>
895
+ # define __CPROVER_STDIO_H_INCLUDED
896
+ #endif
897
+
898
+ #ifndef __CPROVER_STDARG_H_INCLUDED
899
+ # include <stdarg.h>
900
+ # define __CPROVER_STDARG_H_INCLUDED
901
+ #endif
902
+
903
+ int __isoc99_scanf (const char * restrict format , ...)
904
+ {
905
+ __CPROVER_HIDE :;
906
+ va_list list ;
907
+ va_start (list , format );
908
+ int result = vfscanf (stdin , format , list );
909
+ va_end (list );
910
+ return result ;
911
+ }
912
+
891
913
/* FUNCTION: sscanf */
892
914
893
915
#ifndef __CPROVER_STDIO_H_INCLUDED
@@ -910,6 +932,28 @@ __CPROVER_HIDE:;
910
932
return result ;
911
933
}
912
934
935
+ /* FUNCTION: __isoc99_sscanf */
936
+
937
+ #ifndef __CPROVER_STDIO_H_INCLUDED
938
+ # include <stdio.h>
939
+ # define __CPROVER_STDIO_H_INCLUDED
940
+ #endif
941
+
942
+ #ifndef __CPROVER_STDARG_H_INCLUDED
943
+ # include <stdarg.h>
944
+ # define __CPROVER_STDARG_H_INCLUDED
945
+ #endif
946
+
947
+ int __isoc99_sscanf (const char * restrict s , const char * restrict format , ...)
948
+ {
949
+ __CPROVER_HIDE :;
950
+ va_list list ;
951
+ va_start (list , format );
952
+ int result = vsscanf (s , format , list );
953
+ va_end (list );
954
+ return result ;
955
+ }
956
+
913
957
/* FUNCTION: vfscanf */
914
958
915
959
#ifndef __CPROVER_STDIO_H_INCLUDED
@@ -949,6 +993,48 @@ int vfscanf(FILE *restrict stream, const char *restrict format, va_list arg)
949
993
return result ;
950
994
}
951
995
996
+ /* FUNCTION: __isoc99_vfscanf */
997
+
998
+ #ifndef __CPROVER_STDIO_H_INCLUDED
999
+ # include <stdio.h>
1000
+ # define __CPROVER_STDIO_H_INCLUDED
1001
+ #endif
1002
+
1003
+ #ifndef __CPROVER_STDARG_H_INCLUDED
1004
+ # include <stdarg.h>
1005
+ # define __CPROVER_STDARG_H_INCLUDED
1006
+ #endif
1007
+
1008
+ int __VERIFIER_nondet_int ();
1009
+
1010
+ int __isoc99_vfscanf (
1011
+ FILE * restrict stream ,
1012
+ const char * restrict format ,
1013
+ va_list arg )
1014
+ {
1015
+ __CPROVER_HIDE :;
1016
+ int result = __VERIFIER_nondet_int ();
1017
+
1018
+ if (stream != stdin )
1019
+ {
1020
+ #if !defined(__linux__ ) || defined(__GLIBC__ )
1021
+ (void )* stream ;
1022
+ #else
1023
+ (void )* (char * )stream ;
1024
+ #endif
1025
+ }
1026
+
1027
+ (void )* format ;
1028
+ (void )arg ;
1029
+
1030
+ #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
1031
+ __CPROVER_assert (
1032
+ __CPROVER_get_must (stream , "open" ), "vfscanf file must be open" );
1033
+ #endif
1034
+
1035
+ return result ;
1036
+ }
1037
+
952
1038
/* FUNCTION: vscanf */
953
1039
954
1040
#ifndef __CPROVER_STDIO_H_INCLUDED
@@ -967,6 +1053,24 @@ int vscanf(const char *restrict format, va_list arg)
967
1053
return vfscanf (stdin , format , arg );
968
1054
}
969
1055
1056
+ /* FUNCTION: __isoc99_vscanf */
1057
+
1058
+ #ifndef __CPROVER_STDIO_H_INCLUDED
1059
+ # include <stdio.h>
1060
+ # define __CPROVER_STDIO_H_INCLUDED
1061
+ #endif
1062
+
1063
+ #ifndef __CPROVER_STDARG_H_INCLUDED
1064
+ # include <stdarg.h>
1065
+ # define __CPROVER_STDARG_H_INCLUDED
1066
+ #endif
1067
+
1068
+ int __isoc99_vscanf (const char * restrict format , va_list arg )
1069
+ {
1070
+ __CPROVER_HIDE :;
1071
+ return vfscanf (stdin , format , arg );
1072
+ }
1073
+
970
1074
/* FUNCTION: vsscanf */
971
1075
972
1076
#ifndef __CPROVER_STDIO_H_INCLUDED
@@ -991,6 +1095,33 @@ int vsscanf(const char *restrict s, const char *restrict format, va_list arg)
991
1095
return result ;
992
1096
}
993
1097
1098
+ /* FUNCTION: __isoc99_vsscanf */
1099
+
1100
+ #ifndef __CPROVER_STDIO_H_INCLUDED
1101
+ # include <stdio.h>
1102
+ # define __CPROVER_STDIO_H_INCLUDED
1103
+ #endif
1104
+
1105
+ #ifndef __CPROVER_STDARG_H_INCLUDED
1106
+ # include <stdarg.h>
1107
+ # define __CPROVER_STDARG_H_INCLUDED
1108
+ #endif
1109
+
1110
+ int __VERIFIER_nondet_int ();
1111
+
1112
+ int __isoc99_vsscanf (
1113
+ const char * restrict s ,
1114
+ const char * restrict format ,
1115
+ va_list arg )
1116
+ {
1117
+ __CPROVER_HIDE :;
1118
+ int result = __VERIFIER_nondet_int ();
1119
+ (void )* s ;
1120
+ (void )* format ;
1121
+ (void )arg ;
1122
+ return result ;
1123
+ }
1124
+
994
1125
/* FUNCTION: printf */
995
1126
996
1127
#ifndef __CPROVER_STDIO_H_INCLUDED
0 commit comments