|  |  | @ -19,126 +19,112 @@ | 
			
		
	
		
		
			
				
					
					|  |  |  | #define USE_CPP_OVERLOADS |  |  |  | #define USE_CPP_OVERLOADS | 
			
		
	
		
		
			
				
					
					|  |  |  | #endif |  |  |  | #endif | 
			
		
	
		
		
			
				
					
					|  |  |  | 
 |  |  |  | 
 | 
			
		
	
		
		
			
				
					
					|  |  |  | #include <stdio.h> |  |  |  |  | 
			
		
	
		
		
			
				
					
					|  |  |  | #include <stdarg.h> |  |  |  | #include <stdarg.h> | 
			
		
	
		
		
			
				
					
					|  |  |  |  |  |  |  | #include <stdio.h> | 
			
		
	
		
		
			
				
					
					|  |  |  | #include <string.h> |  |  |  | #include <string.h> | 
			
		
	
		
		
			
				
					
					|  |  |  | #include <wchar.h> |  |  |  | #include <wchar.h> | 
			
		
	
		
		
			
				
					
					|  |  |  | 
 |  |  |  | 
 | 
			
		
	
		
		
			
				
					
					|  |  |  | #define restrict |  |  |  | #define restrict | 
			
		
	
		
		
			
				
					
					|  |  |  | 
 |  |  |  | 
 | 
			
		
	
		
		
			
				
					
					|  |  |  | 
 |  |  |  |  | 
			
		
	
		
		
			
				
					
					|  |  |  | #ifdef _WIN32 |  |  |  | #ifdef _WIN32 | 
			
		
	
		
		
			
				
					
					|  |  |  | #define CLIBCALL __cdecl |  |  |  | #define CLIBCALL __cdecl | 
			
		
	
		
		
			
				
					
					|  |  |  | #else |  |  |  | #else | 
			
		
	
		
		
			
				
					
					|  |  |  | #define CLIBCALL |  |  |  | #define CLIBCALL | 
			
		
	
		
		
			
				
					
					|  |  |  | #endif |  |  |  | #endif | 
			
		
	
		
		
			
				
					
					|  |  |  | 
 |  |  |  | 
 | 
			
		
	
		
		
			
				
					
					|  |  |  | int CLIBCALL fwscanf(FILE * restrict stream, const wchar_t * restrict format, ...); // builtin: modeled internally
 |  |  |  | int CLIBCALL fwscanf(FILE* restrict stream, | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  | int CLIBCALL swscanf(const wchar_t * restrict s, const wchar_t * restrict format, ...); // builtin: modeled internally
 |  |  |  |                      const wchar_t* restrict format, | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  | int CLIBCALL vfwscanf(FILE * restrict stream, const wchar_t * restrict format, va_list arg); // builtin: modeled internally
 |  |  |  |                      ...); // builtin: modeled internally
 | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  | int CLIBCALL vswscanf(const wchar_t * restrict s, const wchar_t * restrict format, va_list arg); // builtin: modeled internally
 |  |  |  | int CLIBCALL swscanf(const wchar_t* restrict s, | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  | int CLIBCALL vwscanf(const wchar_t * restrict format, va_list arg); // builtin: modeled internally
 |  |  |  |                      const wchar_t* restrict format, | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  | int CLIBCALL wscanf(const wchar_t * restrict format, ...); // builtin: modeled internally
 |  |  |  |                      ...); // builtin: modeled internally
 | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  | 
 |  |  |  | int CLIBCALL vfwscanf(FILE* restrict stream, | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  | 
 |  |  |  |                       const wchar_t* restrict format, | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  | wint_t CLIBCALL btowc(int c) |  |  |  |                       va_list arg); // builtin: modeled internally
 | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  | { |  |  |  | int CLIBCALL vswscanf(const wchar_t* restrict s, | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  |   return __infer_nondet_int(); |  |  |  |                       const wchar_t* restrict format, | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  | } |  |  |  |                       va_list arg); // builtin: modeled internally
 | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  | 
 |  |  |  | int CLIBCALL vwscanf(const wchar_t* restrict format, | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  | wint_t CLIBCALL fgetwc(FILE *stream) |  |  |  |                      va_list arg); // builtin: modeled internally
 | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  | { |  |  |  | int CLIBCALL wscanf(const wchar_t* restrict format, | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  |   return __infer_nondet_int(); |  |  |  |                     ...); // builtin: modeled internally
 | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  | } |  |  |  | 
 | 
			
				
				
			
		
	
		
		
	
		
		
	
		
		
	
		
		
	
		
		
	
		
		
	
		
		
	
		
		
	
		
		
	
		
		
	
		
		
	
		
		
	
		
		
	
		
		
	
		
		
	
		
		
	
		
		
	
		
		
			
				
					
					|  |  |  |  |  |  |  | wint_t CLIBCALL btowc(int c) { return __infer_nondet_int(); } | 
			
		
	
		
		
			
				
					
					|  |  |  |  |  |  |  | 
 | 
			
		
	
		
		
			
				
					
					|  |  |  |  |  |  |  | wint_t CLIBCALL fgetwc(FILE* stream) { return __infer_nondet_int(); } | 
			
		
	
		
		
			
				
					
					|  |  |  | 
 |  |  |  | 
 | 
			
		
	
		
		
			
				
					
					|  |  |  | // modelled like fgets
 |  |  |  | // modelled like fgets
 | 
			
		
	
		
		
			
				
					
					|  |  |  | wchar_t * CLIBCALL fgetws(wchar_t * restrict s, int n, FILE * restrict stream) |  |  |  | wchar_t* CLIBCALL fgetws(wchar_t* restrict s, int n, FILE* restrict stream) { | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  | { |  |  |  |   return (wchar_t*)fgets((char*)s, n, stream); | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  |   return (wchar_t *) fgets((char *)s, n, stream); |  |  |  |  | 
			
		
	
		
		
	
		
		
	
		
		
			
				
					
					|  |  |  | } |  |  |  | } | 
			
		
	
		
		
			
				
					
					|  |  |  | 
 |  |  |  | 
 | 
			
		
	
		
		
			
				
					
					|  |  |  | wint_t CLIBCALL fputwc(wchar_t c, FILE *stream) |  |  |  | wint_t CLIBCALL fputwc(wchar_t c, FILE* stream) { return __infer_nondet_int(); } | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  | { |  |  |  |  | 
			
		
	
		
		
			
				
					
					|  |  |  |   return __infer_nondet_int(); |  |  |  |  | 
			
		
	
		
		
			
				
					
					|  |  |  | } |  |  |  |  | 
			
		
	
		
		
	
		
		
			
				
					
					|  |  |  | 
 |  |  |  | 
 | 
			
		
	
		
		
			
				
					
					|  |  |  | // modeled using fputs
 |  |  |  | // modeled using fputs
 | 
			
		
	
		
		
			
				
					
					|  |  |  | int CLIBCALL fputws(const wchar_t * restrict s, FILE * restrict stream) |  |  |  | int CLIBCALL fputws(const wchar_t* restrict s, FILE* restrict stream) { | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  | { |  |  |  |   return fputs((char*)s, stream); | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  |   return fputs((char *)s, stream); |  |  |  |  | 
			
		
	
		
		
	
		
		
	
		
		
			
				
					
					|  |  |  | } |  |  |  | } | 
			
		
	
		
		
			
				
					
					|  |  |  | 
 |  |  |  | 
 | 
			
		
	
		
		
			
				
					
					|  |  |  | int CLIBCALL fwide(FILE *stream, int mode) |  |  |  | int CLIBCALL fwide(FILE* stream, int mode) { return __infer_nondet_int(); } | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  | { |  |  |  |  | 
			
		
	
		
		
			
				
					
					|  |  |  |   return __infer_nondet_int(); |  |  |  |  | 
			
		
	
		
		
			
				
					
					|  |  |  | } |  |  |  |  | 
			
		
	
		
		
	
		
		
			
				
					
					|  |  |  | 
 |  |  |  | 
 | 
			
		
	
		
		
			
				
					
					|  |  |  | // return a nondeterministic nonnegative integer
 |  |  |  | // return a nondeterministic nonnegative integer
 | 
			
		
	
		
		
			
				
					
					|  |  |  | int CLIBCALL fwprintf(FILE * restrict stream, const wchar_t * restrict format, ...) |  |  |  | int CLIBCALL fwprintf(FILE* restrict stream, | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  | { |  |  |  |                       const wchar_t* restrict format, | 
			
				
				
			
		
	
		
		
	
		
		
	
		
		
			
				
					
					|  |  |  |  |  |  |  |                       ...) { | 
			
		
	
		
		
			
				
					
					|  |  |  |   int res; |  |  |  |   int res; | 
			
		
	
		
		
			
				
					
					|  |  |  |   res = __infer_nondet_int(); |  |  |  |   res = __infer_nondet_int(); | 
			
		
	
		
		
			
				
					
					|  |  |  |   INFER_EXCLUDE_CONDITION(res < 0); |  |  |  |   INFER_EXCLUDE_CONDITION(res < 0); | 
			
		
	
		
		
			
				
					
					|  |  |  |   return res; |  |  |  |   return res; | 
			
		
	
		
		
			
				
					
					|  |  |  | } |  |  |  | } | 
			
		
	
		
		
			
				
					
					|  |  |  | 
 |  |  |  | 
 | 
			
		
	
		
		
			
				
					
					|  |  |  | 
 |  |  |  |  | 
			
		
	
		
		
			
				
					
					|  |  |  | #ifdef getwc |  |  |  | #ifdef getwc | 
			
		
	
		
		
			
				
					
					|  |  |  | #undef getwc // disable expansion of getwc
 |  |  |  | #undef getwc // disable expansion of getwc
 | 
			
		
	
		
		
			
				
					
					|  |  |  | #endif |  |  |  | #endif | 
			
		
	
		
		
			
				
					
					|  |  |  | wint_t CLIBCALL getwc(FILE *stream) |  |  |  | wint_t CLIBCALL getwc(FILE* stream) { return __infer_nondet_int(); } | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  | { |  |  |  |  | 
			
		
	
		
		
			
				
					
					|  |  |  |   return __infer_nondet_int(); |  |  |  |  | 
			
		
	
		
		
			
				
					
					|  |  |  | } |  |  |  |  | 
			
		
	
		
		
	
		
		
			
				
					
					|  |  |  | 
 |  |  |  | 
 | 
			
		
	
		
		
			
				
					
					|  |  |  | #ifdef getwchar |  |  |  | #ifdef getwchar | 
			
		
	
		
		
			
				
					
					|  |  |  | #undef getwchar // disable expansion of getwchar
 |  |  |  | #undef getwchar // disable expansion of getwchar
 | 
			
		
	
		
		
			
				
					
					|  |  |  | #endif |  |  |  | #endif | 
			
		
	
		
		
			
				
					
					|  |  |  | wint_t CLIBCALL getwchar() |  |  |  | wint_t CLIBCALL getwchar() { return __infer_nondet_int(); } | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  | { |  |  |  |  | 
			
		
	
		
		
			
				
					
					|  |  |  |   return __infer_nondet_int(); |  |  |  |  | 
			
		
	
		
		
			
				
					
					|  |  |  | } |  |  |  |  | 
			
		
	
		
		
	
		
		
			
				
					
					|  |  |  | 
 |  |  |  | 
 | 
			
		
	
		
		
			
				
					
					|  |  |  | size_t CLIBCALL mbrlen(const char * restrict s, size_t n, mbstate_t * restrict ps) |  |  |  | size_t CLIBCALL mbrlen(const char* restrict s, | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  | { |  |  |  |                        size_t n, | 
			
				
				
			
		
	
		
		
	
		
		
	
		
		
			
				
					
					|  |  |  |  |  |  |  |                        mbstate_t* restrict ps) { | 
			
		
	
		
		
			
				
					
					|  |  |  |   return __infer_nondet_int(); |  |  |  |   return __infer_nondet_int(); | 
			
		
	
		
		
			
				
					
					|  |  |  | } |  |  |  | } | 
			
		
	
		
		
			
				
					
					|  |  |  | 
 |  |  |  | 
 | 
			
		
	
		
		
			
				
					
					|  |  |  | size_t CLIBCALL mbrtowc(wchar_t * restrict pwc, const char * restrict s, size_t n, mbstate_t * restrict ps) |  |  |  | size_t CLIBCALL mbrtowc(wchar_t* restrict pwc, | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  | { |  |  |  |                         const char* restrict s, | 
			
				
				
			
		
	
		
		
	
		
		
	
		
		
			
				
					
					|  |  |  |  |  |  |  |                         size_t n, | 
			
		
	
		
		
			
				
					
					|  |  |  |  |  |  |  |                         mbstate_t* restrict ps) { | 
			
		
	
		
		
			
				
					
					|  |  |  |   return __infer_nondet_int(); |  |  |  |   return __infer_nondet_int(); | 
			
		
	
		
		
			
				
					
					|  |  |  | } |  |  |  | } | 
			
		
	
		
		
			
				
					
					|  |  |  | 
 |  |  |  | 
 | 
			
		
	
		
		
			
				
					
					|  |  |  | int CLIBCALL mbsinit(const mbstate_t *ps) |  |  |  | int CLIBCALL mbsinit(const mbstate_t* ps) { return __infer_nondet_int(); } | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  | { |  |  |  |  | 
			
		
	
		
		
			
				
					
					|  |  |  |   return __infer_nondet_int(); |  |  |  |  | 
			
		
	
		
		
			
				
					
					|  |  |  | } |  |  |  |  | 
			
		
	
		
		
	
		
		
			
				
					
					|  |  |  | 
 |  |  |  | 
 | 
			
		
	
		
		
			
				
					
					|  |  |  | size_t CLIBCALL mbsrtowcs(wchar_t * restrict dst, const char ** restrict src, size_t len, mbstate_t * restrict ps) |  |  |  | size_t CLIBCALL mbsrtowcs(wchar_t* restrict dst, | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  | { |  |  |  |                           const char** restrict src, | 
			
				
				
			
		
	
		
		
	
		
		
	
		
		
			
				
					
					|  |  |  |  |  |  |  |                           size_t len, | 
			
		
	
		
		
			
				
					
					|  |  |  |  |  |  |  |                           mbstate_t* restrict ps) { | 
			
		
	
		
		
			
				
					
					|  |  |  |   return __infer_nondet_int(); |  |  |  |   return __infer_nondet_int(); | 
			
		
	
		
		
			
				
					
					|  |  |  | } |  |  |  | } | 
			
		
	
		
		
			
				
					
					|  |  |  | 
 |  |  |  | 
 | 
			
		
	
		
		
			
				
					
					|  |  |  | #ifdef putwc |  |  |  | #ifdef putwc | 
			
		
	
		
		
			
				
					
					|  |  |  | #undef putwc // disable expansion of putwc
 |  |  |  | #undef putwc // disable expansion of putwc
 | 
			
		
	
		
		
			
				
					
					|  |  |  | #endif |  |  |  | #endif | 
			
		
	
		
		
			
				
					
					|  |  |  | wint_t CLIBCALL putwc(wchar_t c, FILE *stream) |  |  |  | wint_t CLIBCALL putwc(wchar_t c, FILE* stream) { return __infer_nondet_int(); } | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  | { |  |  |  |  | 
			
		
	
		
		
			
				
					
					|  |  |  |   return __infer_nondet_int(); |  |  |  |  | 
			
		
	
		
		
			
				
					
					|  |  |  | } |  |  |  |  | 
			
		
	
		
		
	
		
		
			
				
					
					|  |  |  | 
 |  |  |  | 
 | 
			
		
	
		
		
			
				
					
					|  |  |  | #ifdef putwchar |  |  |  | #ifdef putwchar | 
			
		
	
		
		
			
				
					
					|  |  |  | #undef putwchar // disable expansion of putwchar
 |  |  |  | #undef putwchar // disable expansion of putwchar
 | 
			
		
	
		
		
			
				
					
					|  |  |  | #endif |  |  |  | #endif | 
			
		
	
		
		
			
				
					
					|  |  |  | wint_t CLIBCALL putwchar(wchar_t c) |  |  |  | wint_t CLIBCALL putwchar(wchar_t c) { return __infer_nondet_int(); } | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  | { |  |  |  |  | 
			
		
	
		
		
			
				
					
					|  |  |  |   return __infer_nondet_int(); |  |  |  |  | 
			
		
	
		
		
			
				
					
					|  |  |  | } |  |  |  |  | 
			
		
	
		
		
	
		
		
			
				
					
					|  |  |  | 
 |  |  |  | 
 | 
			
		
	
		
		
			
				
					
					|  |  |  | // s must be allocated
 |  |  |  | // s must be allocated
 | 
			
		
	
		
		
			
				
					
					|  |  |  | // return a nondeterministic nonnegative integer
 |  |  |  | // return a nondeterministic nonnegative integer
 | 
			
		
	
		
		
			
				
					
					|  |  |  | int CLIBCALL swprintf(wchar_t * restrict s, size_t n, const wchar_t * restrict format, ...) |  |  |  | int CLIBCALL swprintf(wchar_t* restrict s, | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  | { |  |  |  |                       size_t n, | 
			
				
				
			
		
	
		
		
	
		
		
	
		
		
			
				
					
					|  |  |  |  |  |  |  |                       const wchar_t* restrict format, | 
			
		
	
		
		
			
				
					
					|  |  |  |  |  |  |  |                       ...) { | 
			
		
	
		
		
			
				
					
					|  |  |  |   int res; |  |  |  |   int res; | 
			
		
	
		
		
			
				
					
					|  |  |  |   int size1; |  |  |  |   int size1; | 
			
		
	
		
		
			
				
					
					|  |  |  |   size1 = __get_array_size(s); |  |  |  |   size1 = __get_array_size(s); | 
			
		
	
	
		
		
			
				
					|  |  | @ -147,14 +133,12 @@ int CLIBCALL swprintf(wchar_t * restrict s, size_t n, const wchar_t * restrict f | 
			
		
	
		
		
			
				
					
					|  |  |  |   return res; |  |  |  |   return res; | 
			
		
	
		
		
			
				
					
					|  |  |  | } |  |  |  | } | 
			
		
	
		
		
			
				
					
					|  |  |  | 
 |  |  |  | 
 | 
			
		
	
		
		
			
				
					
					|  |  |  | wint_t CLIBCALL ungetwc(wint_t c, FILE *stream) |  |  |  | wint_t CLIBCALL ungetwc(wint_t c, FILE* stream) { return __infer_nondet_int(); } | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  | { |  |  |  |  | 
			
		
	
		
		
			
				
					
					|  |  |  |   return __infer_nondet_int(); |  |  |  |  | 
			
		
	
		
		
			
				
					
					|  |  |  | } |  |  |  |  | 
			
		
	
		
		
	
		
		
			
				
					
					|  |  |  | 
 |  |  |  | 
 | 
			
		
	
		
		
			
				
					
					|  |  |  | // return a nondeterministic nonnegative integer
 |  |  |  | // return a nondeterministic nonnegative integer
 | 
			
		
	
		
		
			
				
					
					|  |  |  | int CLIBCALL vfwprintf(FILE * restrict stream, const wchar_t * restrict format, va_list arg) |  |  |  | int CLIBCALL vfwprintf(FILE* restrict stream, | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  | { |  |  |  |                        const wchar_t* restrict format, | 
			
				
				
			
		
	
		
		
	
		
		
	
		
		
			
				
					
					|  |  |  |  |  |  |  |                        va_list arg) { | 
			
		
	
		
		
			
				
					
					|  |  |  |   int res; |  |  |  |   int res; | 
			
		
	
		
		
			
				
					
					|  |  |  |   res = __infer_nondet_int(); |  |  |  |   res = __infer_nondet_int(); | 
			
		
	
		
		
			
				
					
					|  |  |  |   INFER_EXCLUDE_CONDITION(res < 0); |  |  |  |   INFER_EXCLUDE_CONDITION(res < 0); | 
			
		
	
	
		
		
			
				
					|  |  | @ -162,8 +146,10 @@ int CLIBCALL vfwprintf(FILE * restrict stream, const wchar_t * restrict format, | 
			
		
	
		
		
			
				
					
					|  |  |  | } |  |  |  | } | 
			
		
	
		
		
			
				
					
					|  |  |  | 
 |  |  |  | 
 | 
			
		
	
		
		
			
				
					
					|  |  |  | // return a nondeterministic nonnegative integer
 |  |  |  | // return a nondeterministic nonnegative integer
 | 
			
		
	
		
		
			
				
					
					|  |  |  | int CLIBCALL vswprintf(wchar_t * restrict s, size_t n, const wchar_t * restrict format, va_list arg) |  |  |  | int CLIBCALL vswprintf(wchar_t* restrict s, | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  | { |  |  |  |                        size_t n, | 
			
				
				
			
		
	
		
		
	
		
		
	
		
		
			
				
					
					|  |  |  |  |  |  |  |                        const wchar_t* restrict format, | 
			
		
	
		
		
			
				
					
					|  |  |  |  |  |  |  |                        va_list arg) { | 
			
		
	
		
		
			
				
					
					|  |  |  |   int res; |  |  |  |   int res; | 
			
		
	
		
		
			
				
					
					|  |  |  |   res = __infer_nondet_int(); |  |  |  |   res = __infer_nondet_int(); | 
			
		
	
		
		
			
				
					
					|  |  |  |   INFER_EXCLUDE_CONDITION(res < 0); |  |  |  |   INFER_EXCLUDE_CONDITION(res < 0); | 
			
		
	
	
		
		
			
				
					|  |  | @ -171,27 +157,26 @@ int CLIBCALL vswprintf(wchar_t * restrict s, size_t n, const wchar_t * restrict | 
			
		
	
		
		
			
				
					
					|  |  |  | } |  |  |  | } | 
			
		
	
		
		
			
				
					
					|  |  |  | 
 |  |  |  | 
 | 
			
		
	
		
		
			
				
					
					|  |  |  | // return a nondeterministic nonnegative integer
 |  |  |  | // return a nondeterministic nonnegative integer
 | 
			
		
	
		
		
			
				
					
					|  |  |  | int CLIBCALL vwprintf(const wchar_t * restrict format, va_list arg) |  |  |  | int CLIBCALL vwprintf(const wchar_t* restrict format, va_list arg) { | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  | { |  |  |  |  | 
			
		
	
		
		
	
		
		
			
				
					
					|  |  |  |   int res; |  |  |  |   int res; | 
			
		
	
		
		
			
				
					
					|  |  |  |   res = __infer_nondet_int(); |  |  |  |   res = __infer_nondet_int(); | 
			
		
	
		
		
			
				
					
					|  |  |  |   INFER_EXCLUDE_CONDITION(res < 0); |  |  |  |   INFER_EXCLUDE_CONDITION(res < 0); | 
			
		
	
		
		
			
				
					
					|  |  |  |   return res; |  |  |  |   return res; | 
			
		
	
		
		
			
				
					
					|  |  |  | } |  |  |  | } | 
			
		
	
		
		
			
				
					
					|  |  |  | 
 |  |  |  | 
 | 
			
		
	
		
		
			
				
					
					|  |  |  | size_t CLIBCALL wcrtomb(char * restrict s, wchar_t wc, mbstate_t * restrict ps) |  |  |  | size_t CLIBCALL wcrtomb(char* restrict s, wchar_t wc, mbstate_t* restrict ps) { | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  | { |  |  |  |  | 
			
		
	
		
		
	
		
		
			
				
					
					|  |  |  |   return __infer_nondet_int(); |  |  |  |   return __infer_nondet_int(); | 
			
		
	
		
		
			
				
					
					|  |  |  | } |  |  |  | } | 
			
		
	
		
		
			
				
					
					|  |  |  | 
 |  |  |  | 
 | 
			
		
	
		
		
			
				
					
					|  |  |  | size_t CLIBCALL wcsrtombs(char * restrict dst, const wchar_t ** restrict src, size_t len, mbstate_t * restrict ps) |  |  |  | size_t CLIBCALL wcsrtombs(char* restrict dst, | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  | { |  |  |  |                           const wchar_t** restrict src, | 
			
				
				
			
		
	
		
		
	
		
		
	
		
		
			
				
					
					|  |  |  |  |  |  |  |                           size_t len, | 
			
		
	
		
		
			
				
					
					|  |  |  |  |  |  |  |                           mbstate_t* restrict ps) { | 
			
		
	
		
		
			
				
					
					|  |  |  |   return __infer_nondet_int(); |  |  |  |   return __infer_nondet_int(); | 
			
		
	
		
		
			
				
					
					|  |  |  | } |  |  |  | } | 
			
		
	
		
		
			
				
					
					|  |  |  | 
 |  |  |  | 
 | 
			
		
	
		
		
			
				
					
					|  |  |  | // return a nondeterministic nonnegative integer
 |  |  |  | // return a nondeterministic nonnegative integer
 | 
			
		
	
		
		
			
				
					
					|  |  |  | int CLIBCALL wprintf(const wchar_t * restrict format, ...) |  |  |  | int CLIBCALL wprintf(const wchar_t* restrict format, ...) { | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  | { |  |  |  |  | 
			
		
	
		
		
	
		
		
			
				
					
					|  |  |  |   int res; |  |  |  |   int res; | 
			
		
	
		
		
			
				
					
					|  |  |  |   res = __infer_nondet_int(); |  |  |  |   res = __infer_nondet_int(); | 
			
		
	
		
		
			
				
					
					|  |  |  |   INFER_EXCLUDE_CONDITION(res < 0); |  |  |  |   INFER_EXCLUDE_CONDITION(res < 0); | 
			
		
	
	
		
		
			
				
					|  |  | @ -199,41 +184,39 @@ int CLIBCALL wprintf(const wchar_t * restrict format, ...) | 
			
		
	
		
		
			
				
					
					|  |  |  | } |  |  |  | } | 
			
		
	
		
		
			
				
					
					|  |  |  | 
 |  |  |  | 
 | 
			
		
	
		
		
			
				
					
					|  |  |  | // modeled using strcat
 |  |  |  | // modeled using strcat
 | 
			
		
	
		
		
			
				
					
					|  |  |  | wchar_t * CLIBCALL wcscat(wchar_t * restrict s1, const wchar_t * restrict s2) |  |  |  | wchar_t* CLIBCALL wcscat(wchar_t* restrict s1, const wchar_t* restrict s2) { | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  | { |  |  |  |   return (wchar_t*)strcat((char*)s1, (char*)s2); | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  |   return (wchar_t *) strcat((char *) s1, (char *) s2); |  |  |  |  | 
			
		
	
		
		
	
		
		
	
		
		
			
				
					
					|  |  |  | } |  |  |  | } | 
			
		
	
		
		
			
				
					
					|  |  |  | 
 |  |  |  | 
 | 
			
		
	
		
		
			
				
					
					|  |  |  | // modeled using strchr
 |  |  |  | // modeled using strchr
 | 
			
		
	
		
		
			
				
					
					|  |  |  | #ifndef USE_CPP_OVERLOADS |  |  |  | #ifndef USE_CPP_OVERLOADS | 
			
		
	
		
		
			
				
					
					|  |  |  | wchar_t * CLIBCALL wcschr(const wchar_t *s, wchar_t c) |  |  |  | wchar_t* CLIBCALL wcschr(const wchar_t* s, wchar_t c) | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  | # else |  |  |  | #else | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  | const wchar_t * CLIBCALL wcschr(const wchar_t *s, wchar_t c) |  |  |  | const wchar_t* CLIBCALL wcschr(const wchar_t* s, wchar_t c) { | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  | { |  |  |  |   return wcschr((wchar_t*)s, c); | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  |   return wcschr((wchar_t*) s, c); |  |  |  |  | 
			
		
	
		
		
	
		
		
	
		
		
	
		
		
	
		
		
			
				
					
					|  |  |  | } |  |  |  | } | 
			
		
	
		
		
			
				
					
					|  |  |  | 
 |  |  |  | 
 | 
			
		
	
		
		
			
				
					
					|  |  |  | wchar_t * CLIBCALL wcschr(wchar_t *s, wchar_t c) |  |  |  | wchar_t* CLIBCALL wcschr(wchar_t* s, wchar_t c) | 
			
				
				
			
		
	
		
		
	
		
		
			
				
					
					|  |  |  | #endif |  |  |  | #endif | 
			
		
	
		
		
			
				
					
					|  |  |  | { |  |  |  | { | 
			
		
	
		
		
			
				
					
					|  |  |  |   return (wchar_t *) strchr((char *) s, c); |  |  |  |   return (wchar_t*)strchr((char*)s, c); | 
			
				
				
			
		
	
		
		
	
		
		
			
				
					
					|  |  |  | } |  |  |  | } | 
			
		
	
		
		
			
				
					
					|  |  |  | 
 |  |  |  | 
 | 
			
		
	
		
		
			
				
					
					|  |  |  | // modeled using strcmp
 |  |  |  | // modeled using strcmp
 | 
			
		
	
		
		
			
				
					
					|  |  |  | int CLIBCALL wcscmp(const wchar_t *s1, const wchar_t *s2) |  |  |  | int CLIBCALL wcscmp(const wchar_t* s1, const wchar_t* s2) { | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  | { |  |  |  |   return strcmp((char*)s1, (char*)s2); | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  |   return strcmp((char *) s1, (char *) s2); |  |  |  |  | 
			
		
	
		
		
	
		
		
	
		
		
			
				
					
					|  |  |  | } |  |  |  | } | 
			
		
	
		
		
			
				
					
					|  |  |  | 
 |  |  |  | 
 | 
			
		
	
		
		
			
				
					
					|  |  |  | // modeled using strcmp
 |  |  |  | // modeled using strcmp
 | 
			
		
	
		
		
			
				
					
					|  |  |  | int CLIBCALL wcscoll(const wchar_t *s1, const wchar_t *s2) |  |  |  | int CLIBCALL wcscoll(const wchar_t* s1, const wchar_t* s2) { | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  | { |  |  |  |   return strcmp((char*)s1, (char*)s2); | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  |   return strcmp((char *) s1, (char *) s2); |  |  |  |  | 
			
		
	
		
		
	
		
		
	
		
		
			
				
					
					|  |  |  | } |  |  |  | } | 
			
		
	
		
		
			
				
					
					|  |  |  | 
 |  |  |  | 
 | 
			
		
	
		
		
			
				
					
					|  |  |  | // return a nondeterministic nonnegative integer
 |  |  |  | // return a nondeterministic nonnegative integer
 | 
			
		
	
		
		
			
				
					
					|  |  |  | size_t CLIBCALL wcsftime(wchar_t * restrict s, size_t maxsize,const wchar_t * restrict format, const struct tm * restrict timeptr) |  |  |  | size_t CLIBCALL wcsftime(wchar_t* restrict s, | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  | { |  |  |  |                          size_t maxsize, | 
			
				
				
			
		
	
		
		
	
		
		
	
		
		
			
				
					
					|  |  |  |  |  |  |  |                          const wchar_t* restrict format, | 
			
		
	
		
		
			
				
					
					|  |  |  |  |  |  |  |                          const struct tm* restrict timeptr) { | 
			
		
	
		
		
			
				
					
					|  |  |  |   int res; |  |  |  |   int res; | 
			
		
	
		
		
			
				
					
					|  |  |  |   res = __infer_nondet_int(); |  |  |  |   res = __infer_nondet_int(); | 
			
		
	
		
		
			
				
					
					|  |  |  |   INFER_EXCLUDE_CONDITION(res < 0); |  |  |  |   INFER_EXCLUDE_CONDITION(res < 0); | 
			
		
	
	
		
		
			
				
					|  |  | @ -241,178 +224,169 @@ size_t CLIBCALL wcsftime(wchar_t * restrict s, size_t maxsize,const wchar_t * re | 
			
		
	
		
		
			
				
					
					|  |  |  | } |  |  |  | } | 
			
		
	
		
		
			
				
					
					|  |  |  | 
 |  |  |  | 
 | 
			
		
	
		
		
			
				
					
					|  |  |  | // modeled using strcpy
 |  |  |  | // modeled using strcpy
 | 
			
		
	
		
		
			
				
					
					|  |  |  | wchar_t * CLIBCALL wcscpy(wchar_t * restrict s1, const wchar_t * restrict s2) |  |  |  | wchar_t* CLIBCALL wcscpy(wchar_t* restrict s1, const wchar_t* restrict s2) { | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  | { |  |  |  |   return (wchar_t*)strcpy((char*)s1, (char*)s2); | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  |   return (wchar_t *) strcpy((char *) s1, (char *) s2); |  |  |  |  | 
			
		
	
		
		
	
		
		
	
		
		
			
				
					
					|  |  |  | } |  |  |  | } | 
			
		
	
		
		
			
				
					
					|  |  |  | 
 |  |  |  | 
 | 
			
		
	
		
		
			
				
					
					|  |  |  | // modeled using strcmp
 |  |  |  | // modeled using strcmp
 | 
			
		
	
		
		
			
				
					
					|  |  |  | size_t CLIBCALL wcscspn(const wchar_t *s1, const wchar_t *s2) |  |  |  | size_t CLIBCALL wcscspn(const wchar_t* s1, const wchar_t* s2) { | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  | { |  |  |  |   return strcmp((char*)s1, (char*)s2); | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  |   return strcmp((char *) s1, (char *) s2); |  |  |  |  | 
			
		
	
		
		
	
		
		
	
		
		
			
				
					
					|  |  |  | } |  |  |  | } | 
			
		
	
		
		
			
				
					
					|  |  |  | 
 |  |  |  | 
 | 
			
		
	
		
		
			
				
					
					|  |  |  | // modeled using strlen
 |  |  |  | // modeled using strlen
 | 
			
		
	
		
		
			
				
					
					|  |  |  | size_t CLIBCALL wcslen(const wchar_t *s) |  |  |  | size_t CLIBCALL wcslen(const wchar_t* s) { return strlen((char*)s); } | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  | { |  |  |  |  | 
			
		
	
		
		
			
				
					
					|  |  |  |   return strlen((char *) s); |  |  |  |  | 
			
		
	
		
		
			
				
					
					|  |  |  | } |  |  |  |  | 
			
		
	
		
		
	
		
		
			
				
					
					|  |  |  | 
 |  |  |  | 
 | 
			
		
	
		
		
			
				
					
					|  |  |  | // modeled using strncat
 |  |  |  | // modeled using strncat
 | 
			
		
	
		
		
			
				
					
					|  |  |  | wchar_t * CLIBCALL wcsncat(wchar_t * restrict s1, const wchar_t * restrict s2, size_t n) |  |  |  | wchar_t* CLIBCALL wcsncat(wchar_t* restrict s1, | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  | { |  |  |  |                           const wchar_t* restrict s2, | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  |   return (wchar_t *) strncat((char *) s1, (char *) s2, n); |  |  |  |                           size_t n) { | 
			
				
				
			
		
	
		
		
	
		
		
	
		
		
	
		
		
			
				
					
					|  |  |  |  |  |  |  |   return (wchar_t*)strncat((char*)s1, (char*)s2, n); | 
			
		
	
		
		
			
				
					
					|  |  |  | } |  |  |  | } | 
			
		
	
		
		
			
				
					
					|  |  |  | 
 |  |  |  | 
 | 
			
		
	
		
		
			
				
					
					|  |  |  | // modeled using strncmp
 |  |  |  | // modeled using strncmp
 | 
			
		
	
		
		
			
				
					
					|  |  |  | int CLIBCALL wcsncmp(const wchar_t *s1, const wchar_t *s2, size_t n) |  |  |  | int CLIBCALL wcsncmp(const wchar_t* s1, const wchar_t* s2, size_t n) { | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  | { |  |  |  |   return strncmp((char*)s1, (char*)s2, n); | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  |   return strncmp((char *) s1, (char *) s2, n); |  |  |  |  | 
			
		
	
		
		
	
		
		
	
		
		
			
				
					
					|  |  |  | } |  |  |  | } | 
			
		
	
		
		
			
				
					
					|  |  |  | 
 |  |  |  | 
 | 
			
		
	
		
		
			
				
					
					|  |  |  | // modeled using strpbrk
 |  |  |  | // modeled using strpbrk
 | 
			
		
	
		
		
			
				
					
					|  |  |  | #ifndef USE_CPP_OVERLOADS |  |  |  | #ifndef USE_CPP_OVERLOADS | 
			
		
	
		
		
			
				
					
					|  |  |  | wchar_t * CLIBCALL wcspbrk(const wchar_t *s1, const wchar_t *s2) |  |  |  | wchar_t* CLIBCALL wcspbrk(const wchar_t* s1, const wchar_t* s2) | 
			
				
				
			
		
	
		
		
	
		
		
			
				
					
					|  |  |  | #else |  |  |  | #else | 
			
		
	
		
		
			
				
					
					|  |  |  | const wchar_t * CLIBCALL wcspbrk(const wchar_t *s1, const wchar_t *s2) |  |  |  | const wchar_t* CLIBCALL wcspbrk(const wchar_t* s1, const wchar_t* s2) { | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  | { |  |  |  |   return wcspbrk((wchar_t*)s1, s2); | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  |   return wcspbrk((wchar_t*) s1, s2); |  |  |  |  | 
			
		
	
		
		
	
		
		
	
		
		
			
				
					
					|  |  |  | } |  |  |  | } | 
			
		
	
		
		
			
				
					
					|  |  |  | wchar_t * CLIBCALL wcspbrk(wchar_t *s1, const wchar_t *s2) |  |  |  | wchar_t* CLIBCALL wcspbrk(wchar_t* s1, const wchar_t* s2) | 
			
				
				
			
		
	
		
		
	
		
		
			
				
					
					|  |  |  | #endif |  |  |  | #endif | 
			
		
	
		
		
			
				
					
					|  |  |  | { |  |  |  | { | 
			
		
	
		
		
			
				
					
					|  |  |  |   return (wchar_t *) strpbrk((char *) s1, (char *) s2); |  |  |  |   return (wchar_t*)strpbrk((char*)s1, (char*)s2); | 
			
				
				
			
		
	
		
		
	
		
		
			
				
					
					|  |  |  | } |  |  |  | } | 
			
		
	
		
		
			
				
					
					|  |  |  | 
 |  |  |  | 
 | 
			
		
	
		
		
			
				
					
					|  |  |  | // modeled using strchr
 |  |  |  | // modeled using strchr
 | 
			
		
	
		
		
			
				
					
					|  |  |  | #ifndef USE_CPP_OVERLOADS |  |  |  | #ifndef USE_CPP_OVERLOADS | 
			
		
	
		
		
			
				
					
					|  |  |  | wchar_t * CLIBCALL wcsrchr(const wchar_t *s, wchar_t c) |  |  |  | wchar_t* CLIBCALL wcsrchr(const wchar_t* s, wchar_t c) | 
			
				
				
			
		
	
		
		
	
		
		
			
				
					
					|  |  |  | #else |  |  |  | #else | 
			
		
	
		
		
			
				
					
					|  |  |  | const wchar_t * CLIBCALL wcsrchr(const wchar_t *s, wchar_t c) |  |  |  | const wchar_t* CLIBCALL wcsrchr(const wchar_t* s, wchar_t c) { | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  | { |  |  |  |   return wcsrchr((wchar_t*)s, c); | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  |   return wcsrchr((wchar_t*) s, c); |  |  |  |  | 
			
		
	
		
		
	
		
		
	
		
		
			
				
					
					|  |  |  | } |  |  |  | } | 
			
		
	
		
		
			
				
					
					|  |  |  | 
 |  |  |  | 
 | 
			
		
	
		
		
			
				
					
					|  |  |  | wchar_t * CLIBCALL wcsrchr(wchar_t *s, wchar_t c) |  |  |  | wchar_t* CLIBCALL wcsrchr(wchar_t* s, wchar_t c) | 
			
				
				
			
		
	
		
		
	
		
		
			
				
					
					|  |  |  | #endif |  |  |  | #endif | 
			
		
	
		
		
			
				
					
					|  |  |  | { |  |  |  | { | 
			
		
	
		
		
			
				
					
					|  |  |  |   return (wchar_t *) strchr((char *) s, c); |  |  |  |   return (wchar_t*)strchr((char*)s, c); | 
			
				
				
			
		
	
		
		
	
		
		
			
				
					
					|  |  |  | } |  |  |  | } | 
			
		
	
		
		
			
				
					
					|  |  |  | 
 |  |  |  | 
 | 
			
		
	
		
		
			
				
					
					|  |  |  | // modeled using strncpy
 |  |  |  | // modeled using strncpy
 | 
			
		
	
		
		
			
				
					
					|  |  |  | wchar_t * CLIBCALL wcsncpy(wchar_t * restrict s1, const wchar_t * restrict s2, size_t n) |  |  |  | wchar_t* CLIBCALL wcsncpy(wchar_t* restrict s1, | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  | { |  |  |  |                           const wchar_t* restrict s2, | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  |   return (wchar_t *) strncpy((char *) s1, (char *) s2, n); |  |  |  |                           size_t n) { | 
			
				
				
			
		
	
		
		
	
		
		
	
		
		
	
		
		
			
				
					
					|  |  |  |  |  |  |  |   return (wchar_t*)strncpy((char*)s1, (char*)s2, n); | 
			
		
	
		
		
			
				
					
					|  |  |  | } |  |  |  | } | 
			
		
	
		
		
			
				
					
					|  |  |  | 
 |  |  |  | 
 | 
			
		
	
		
		
			
				
					
					|  |  |  | // modeled using strspn
 |  |  |  | // modeled using strspn
 | 
			
		
	
		
		
			
				
					
					|  |  |  | size_t CLIBCALL wcsspn(const wchar_t *s1, const wchar_t *s2) |  |  |  | size_t CLIBCALL wcsspn(const wchar_t* s1, const wchar_t* s2) { | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  | { |  |  |  |   return strspn((char*)s1, (char*)s2); | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  |   return strspn((char *) s1, (char *) s2); |  |  |  |  | 
			
		
	
		
		
	
		
		
	
		
		
			
				
					
					|  |  |  | } |  |  |  | } | 
			
		
	
		
		
			
				
					
					|  |  |  | 
 |  |  |  | 
 | 
			
		
	
		
		
			
				
					
					|  |  |  | // modeled using strstr
 |  |  |  | // modeled using strstr
 | 
			
		
	
		
		
			
				
					
					|  |  |  | #ifndef USE_CPP_OVERLOADS |  |  |  | #ifndef USE_CPP_OVERLOADS | 
			
		
	
		
		
			
				
					
					|  |  |  | wchar_t * CLIBCALL wcsstr(const wchar_t *s1, const wchar_t *s2) |  |  |  | wchar_t* CLIBCALL wcsstr(const wchar_t* s1, const wchar_t* s2) | 
			
				
				
			
		
	
		
		
	
		
		
			
				
					
					|  |  |  | #else |  |  |  | #else | 
			
		
	
		
		
			
				
					
					|  |  |  | 
 |  |  |  | 
 | 
			
		
	
		
		
			
				
					
					|  |  |  | const wchar_t * CLIBCALL wcsstr(const wchar_t *s1, const wchar_t *s2) |  |  |  | const wchar_t* CLIBCALL wcsstr(const wchar_t* s1, const wchar_t* s2) { | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  | { |  |  |  |   return wcsstr((wchar_t*)s1, s2); | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  |   return wcsstr((wchar_t*) s1, s2); |  |  |  |  | 
			
		
	
		
		
	
		
		
	
		
		
			
				
					
					|  |  |  | } |  |  |  | } | 
			
		
	
		
		
			
				
					
					|  |  |  | wchar_t * CLIBCALL wcsstr(wchar_t *s1, const wchar_t *s2) |  |  |  | wchar_t* CLIBCALL wcsstr(wchar_t* s1, const wchar_t* s2) | 
			
				
				
			
		
	
		
		
	
		
		
			
				
					
					|  |  |  | #endif |  |  |  | #endif | 
			
		
	
		
		
			
				
					
					|  |  |  | { |  |  |  | { | 
			
		
	
		
		
			
				
					
					|  |  |  |   return (wchar_t *) strstr((char *) s1, (char *) s2); |  |  |  |   return (wchar_t*)strstr((char*)s1, (char*)s2); | 
			
				
				
			
		
	
		
		
	
		
		
			
				
					
					|  |  |  | } |  |  |  | } | 
			
		
	
		
		
			
				
					
					|  |  |  | 
 |  |  |  | 
 | 
			
		
	
		
		
			
				
					
					|  |  |  | int CLIBCALL wctob(wint_t c) |  |  |  | int CLIBCALL wctob(wint_t c) { return __infer_nondet_int(); } | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  | { |  |  |  |  | 
			
		
	
		
		
			
				
					
					|  |  |  |   return __infer_nondet_int(); |  |  |  |  | 
			
		
	
		
		
			
				
					
					|  |  |  | } |  |  |  |  | 
			
		
	
		
		
	
		
		
			
				
					
					|  |  |  | 
 |  |  |  | 
 | 
			
		
	
		
		
			
				
					
					|  |  |  | double CLIBCALL wcstod(const wchar_t * restrict nptr, wchar_t ** restrict endptr) |  |  |  | double CLIBCALL wcstod(const wchar_t* restrict nptr, | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  | { |  |  |  |                        wchar_t** restrict endptr) { | 
			
				
				
			
		
	
		
		
	
		
		
	
		
		
			
				
					
					|  |  |  |   return __infer_nondet_double(); |  |  |  |   return __infer_nondet_double(); | 
			
		
	
		
		
			
				
					
					|  |  |  | } |  |  |  | } | 
			
		
	
		
		
			
				
					
					|  |  |  | 
 |  |  |  | 
 | 
			
		
	
		
		
			
				
					
					|  |  |  | float CLIBCALL wcstof(const wchar_t * restrict nptr, wchar_t ** restrict endptr) |  |  |  | float CLIBCALL wcstof(const wchar_t* restrict nptr, wchar_t** restrict endptr) { | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  | { |  |  |  |  | 
			
		
	
		
		
	
		
		
			
				
					
					|  |  |  |   return __infer_nondet_float(); |  |  |  |   return __infer_nondet_float(); | 
			
		
	
		
		
			
				
					
					|  |  |  | } |  |  |  | } | 
			
		
	
		
		
			
				
					
					|  |  |  | 
 |  |  |  | 
 | 
			
		
	
		
		
			
				
					
					|  |  |  | // simplified modeling which returns s1
 |  |  |  | // simplified modeling which returns s1
 | 
			
		
	
		
		
			
				
					
					|  |  |  | wchar_t * CLIBCALL wcstok(wchar_t * restrict s1, const wchar_t * restrict s2, wchar_t ** restrict ptr) |  |  |  | wchar_t* CLIBCALL wcstok(wchar_t* restrict s1, | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  | { |  |  |  |                          const wchar_t* restrict s2, | 
			
				
				
			
		
	
		
		
	
		
		
	
		
		
			
				
					
					|  |  |  |  |  |  |  |                          wchar_t** restrict ptr) { | 
			
		
	
		
		
			
				
					
					|  |  |  |   return s1; |  |  |  |   return s1; | 
			
		
	
		
		
			
				
					
					|  |  |  | } |  |  |  | } | 
			
		
	
		
		
			
				
					
					|  |  |  | 
 |  |  |  | 
 | 
			
		
	
		
		
			
				
					
					|  |  |  | long double CLIBCALL wcstold(const wchar_t * restrict nptr, wchar_t ** restrict endptr) |  |  |  | long double CLIBCALL wcstold(const wchar_t* restrict nptr, | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  | { |  |  |  |                              wchar_t** restrict endptr) { | 
			
				
				
			
		
	
		
		
	
		
		
	
		
		
			
				
					
					|  |  |  |   return __infer_nondet_long_double(); |  |  |  |   return __infer_nondet_long_double(); | 
			
		
	
		
		
			
				
					
					|  |  |  | } |  |  |  | } | 
			
		
	
		
		
			
				
					
					|  |  |  | 
 |  |  |  | 
 | 
			
		
	
		
		
			
				
					
					|  |  |  | long int CLIBCALL wcstol(const wchar_t * restrict nptr, wchar_t ** restrict endptr, int base) |  |  |  | long int CLIBCALL wcstol(const wchar_t* restrict nptr, | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  | { |  |  |  |                          wchar_t** restrict endptr, | 
			
				
				
			
		
	
		
		
	
		
		
	
		
		
			
				
					
					|  |  |  |  |  |  |  |                          int base) { | 
			
		
	
		
		
			
				
					
					|  |  |  |   return __infer_nondet_long_int(); |  |  |  |   return __infer_nondet_long_int(); | 
			
		
	
		
		
			
				
					
					|  |  |  | } |  |  |  | } | 
			
		
	
		
		
			
				
					
					|  |  |  | 
 |  |  |  | 
 | 
			
		
	
		
		
			
				
					
					|  |  |  | long long int CLIBCALL wcstoll(const wchar_t * restrict nptr, wchar_t ** restrict endptr, int base) |  |  |  | long long int CLIBCALL wcstoll(const wchar_t* restrict nptr, | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  | { |  |  |  |                                wchar_t** restrict endptr, | 
			
				
				
			
		
	
		
		
	
		
		
	
		
		
			
				
					
					|  |  |  |  |  |  |  |                                int base) { | 
			
		
	
		
		
			
				
					
					|  |  |  |   return __infer_nondet_long_long_int(); |  |  |  |   return __infer_nondet_long_long_int(); | 
			
		
	
		
		
			
				
					
					|  |  |  | } |  |  |  | } | 
			
		
	
		
		
			
				
					
					|  |  |  | 
 |  |  |  | 
 | 
			
		
	
		
		
			
				
					
					|  |  |  | unsigned long int CLIBCALL wcstoul(const wchar_t * restrict nptr, wchar_t ** restrict endptr, int base) |  |  |  | unsigned long int CLIBCALL wcstoul(const wchar_t* restrict nptr, | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  | { |  |  |  |                                    wchar_t** restrict endptr, | 
			
				
				
			
		
	
		
		
	
		
		
	
		
		
			
				
					
					|  |  |  |  |  |  |  |                                    int base) { | 
			
		
	
		
		
			
				
					
					|  |  |  |   return __infer_nondet_unsigned_long_int(); |  |  |  |   return __infer_nondet_unsigned_long_int(); | 
			
		
	
		
		
			
				
					
					|  |  |  | } |  |  |  | } | 
			
		
	
		
		
			
				
					
					|  |  |  | 
 |  |  |  | 
 | 
			
		
	
		
		
			
				
					
					|  |  |  | unsigned long long int CLIBCALL wcstoull(const wchar_t * restrict nptr, wchar_t ** restrict endptr, int base) |  |  |  | unsigned long long int CLIBCALL wcstoull(const wchar_t* restrict nptr, | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  | { |  |  |  |                                          wchar_t** restrict endptr, | 
			
				
				
			
		
	
		
		
	
		
		
	
		
		
			
				
					
					|  |  |  |  |  |  |  |                                          int base) { | 
			
		
	
		
		
			
				
					
					|  |  |  |   return __infer_nondet_long_long_int(); |  |  |  |   return __infer_nondet_long_long_int(); | 
			
		
	
		
		
			
				
					
					|  |  |  | } |  |  |  | } | 
			
		
	
		
		
			
				
					
					|  |  |  | 
 |  |  |  | 
 | 
			
		
	
		
		
			
				
					
					|  |  |  | // modeled using strncmp
 |  |  |  | // modeled using strncmp
 | 
			
		
	
		
		
			
				
					
					|  |  |  | size_t CLIBCALL wcsxfrm(wchar_t * restrict s1, const wchar_t * restrict s2, size_t n) |  |  |  | size_t CLIBCALL wcsxfrm(wchar_t* restrict s1, | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  | { |  |  |  |                         const wchar_t* restrict s2, | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  |   return strncmp((char *) s1, (char *) s2, n); |  |  |  |                         size_t n) { | 
			
				
				
			
		
	
		
		
	
		
		
	
		
		
	
		
		
			
				
					
					|  |  |  |  |  |  |  |   return strncmp((char*)s1, (char*)s2, n); | 
			
		
	
		
		
			
				
					
					|  |  |  | } |  |  |  | } | 
			
		
	
		
		
			
				
					
					|  |  |  | 
 |  |  |  | 
 | 
			
		
	
		
		
			
				
					
					|  |  |  | // modeled using memchr
 |  |  |  | // modeled using memchr
 | 
			
		
	
		
		
			
				
					
					|  |  |  | #ifndef USE_CPP_OVERLOADS |  |  |  | #ifndef USE_CPP_OVERLOADS | 
			
		
	
		
		
			
				
					
					|  |  |  | wchar_t * CLIBCALL wmemchr(const wchar_t *s, wchar_t c, size_t n) |  |  |  | wchar_t* CLIBCALL wmemchr(const wchar_t* s, wchar_t c, size_t n) | 
			
				
				
			
		
	
		
		
	
		
		
			
				
					
					|  |  |  | #else |  |  |  | #else | 
			
		
	
		
		
			
				
					
					|  |  |  | 
 |  |  |  | 
 | 
			
		
	
		
		
			
				
					
					|  |  |  | const wchar_t * CLIBCALL wmemchr(const wchar_t *s, wchar_t c, size_t n) |  |  |  | const wchar_t* CLIBCALL wmemchr(const wchar_t* s, wchar_t c, size_t n) { | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  | { |  |  |  |   return wmemchr((wchar_t*)s, c, n); | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  |   return wmemchr((wchar_t*) s, c, n); |  |  |  |  | 
			
		
	
		
		
	
		
		
	
		
		
			
				
					
					|  |  |  | } |  |  |  | } | 
			
		
	
		
		
			
				
					
					|  |  |  | wchar_t * CLIBCALL wmemchr(wchar_t *s, wchar_t c, size_t n) |  |  |  | wchar_t* CLIBCALL wmemchr(wchar_t* s, wchar_t c, size_t n) | 
			
				
				
			
		
	
		
		
	
		
		
			
				
					
					|  |  |  | #endif |  |  |  | #endif | 
			
		
	
		
		
			
				
					
					|  |  |  | { |  |  |  | { | 
			
		
	
		
		
			
				
					
					|  |  |  |   return (wchar_t *) memchr((char *) s, c, n); |  |  |  |   return (wchar_t*)memchr((char*)s, c, n); | 
			
				
				
			
		
	
		
		
	
		
		
			
				
					
					|  |  |  | } |  |  |  | } | 
			
		
	
		
		
			
				
					
					|  |  |  | 
 |  |  |  | 
 | 
			
		
	
		
		
			
				
					
					|  |  |  | // modeled using memcmp
 |  |  |  | // modeled using memcmp
 | 
			
		
	
		
		
			
				
					
					|  |  |  | int CLIBCALL wmemcmp(const wchar_t *s1, const wchar_t *s2, size_t n) |  |  |  | int CLIBCALL wmemcmp(const wchar_t* s1, const wchar_t* s2, size_t n) { | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  | { |  |  |  |   return memcmp((char*)s1, (char*)s2, n); | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  |   return memcmp((char *) s1, (char *) s2, n); |  |  |  |  | 
			
		
	
		
		
	
		
		
	
		
		
			
				
					
					|  |  |  | } |  |  |  | } | 
			
		
	
		
		
			
				
					
					|  |  |  | 
 |  |  |  | 
 | 
			
		
	
		
		
			
				
					
					|  |  |  | // modeled using memcpy
 |  |  |  | // modeled using memcpy
 | 
			
		
	
		
		
			
				
					
					|  |  |  | wchar_t * CLIBCALL wmemcpy(wchar_t * restrict s1, const wchar_t * restrict s2, size_t n) |  |  |  | wchar_t* CLIBCALL wmemcpy(wchar_t* restrict s1, | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  | { |  |  |  |                           const wchar_t* restrict s2, | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  |   return (wchar_t *) memcpy((char *) s1, (char *) s2, n); |  |  |  |                           size_t n) { | 
			
				
				
			
		
	
		
		
	
		
		
	
		
		
	
		
		
			
				
					
					|  |  |  |  |  |  |  |   return (wchar_t*)memcpy((char*)s1, (char*)s2, n); | 
			
		
	
		
		
			
				
					
					|  |  |  | } |  |  |  | } | 
			
		
	
		
		
			
				
					
					|  |  |  | 
 |  |  |  | 
 | 
			
		
	
		
		
			
				
					
					|  |  |  | // modeled using memmove
 |  |  |  | // modeled using memmove
 | 
			
		
	
		
		
			
				
					
					|  |  |  | wchar_t * CLIBCALL wmemmove(wchar_t *s1, const wchar_t *s2, size_t n) |  |  |  | wchar_t* CLIBCALL wmemmove(wchar_t* s1, const wchar_t* s2, size_t n) { | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  | { |  |  |  |   return (wchar_t*)memmove((char*)s1, (char*)s2, n); | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  |   return (wchar_t *) memmove((char *) s1, (char *) s2, n); |  |  |  |  | 
			
		
	
		
		
	
		
		
	
		
		
			
				
					
					|  |  |  | } |  |  |  | } | 
			
		
	
		
		
			
				
					
					|  |  |  | 
 |  |  |  | 
 | 
			
		
	
		
		
			
				
					
					|  |  |  | // modeled using memset
 |  |  |  | // modeled using memset
 | 
			
		
	
		
		
			
				
					
					|  |  |  | wchar_t * CLIBCALL wmemset(wchar_t *s, wchar_t c, size_t n) |  |  |  | wchar_t* CLIBCALL wmemset(wchar_t* s, wchar_t c, size_t n) { | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  | { |  |  |  |   return (wchar_t*)memset((char*)s, c, n); | 
			
				
				
			
		
	
		
		
			
				
					
					|  |  |  |   return (wchar_t *) memset((char *) s, c, n); |  |  |  |  | 
			
		
	
		
		
	
		
		
	
		
		
			
				
					
					|  |  |  | } |  |  |  | } | 
			
		
	
	
		
		
			
				
					|  |  | 
 |