CBMC
locale.c
Go to the documentation of this file.
1 
2 /* FUNCTION: setlocale */
3 
4 #ifndef __CPROVER_LOCALE_H_INCLUDED
5 #include <locale.h>
6 #define __CPROVER_LOCALE_H_INCLUDED
7 #endif
8 
9 char *setlocale(int category, const char *locale)
10 {
11  __CPROVER_HIDE:;
12  (void)category;
13  (void)*locale;
14  #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
15  __CPROVER_event("invalidate_pointer", "setlocale_result");
16  char *setlocale_result;
17  __CPROVER_set_may(setlocale_result, "setlocale_result");
18  return setlocale_result;
19  #else
20  static char setlocale_result[1];
21  return setlocale_result;
22  #endif
23 }
24 
25 /* FUNCTION: localeconv */
26 
27 #ifndef __CPROVER_LOCALE_H_INCLUDED
28 #include <locale.h>
29 #define __CPROVER_LOCALE_H_INCLUDED
30 #endif
31 
32 struct lconv *localeconv(void)
33 {
34  __CPROVER_HIDE:;
35  #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
36  __CPROVER_event("invalidate_pointer", "localeconv_result");
37  struct lconv *localeconv_result;
38  __CPROVER_set_may(localeconv_result, "localeconv_result");
39  return localeconv_result;
40  #else
41  static struct lconv localeconv_result;
42  return &localeconv_result;
43  #endif
44 }
__CPROVER_set_may
void __CPROVER_set_may(const void *, const char *)
localeconv
struct lconv * localeconv(void)
Definition: locale.c:32
setlocale
char * setlocale(int category, const char *locale)
Definition: locale.c:9