CBMC
•All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
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
9char *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
32struct 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}
ait
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
ait::ait
ait()
Definition ai.h:565
__CPROVER_set_may
void __CPROVER_set_may(const void *, const char *)
setlocale
char * setlocale(int category, const char *locale)
Definition locale.c:9
localeconv
struct lconv * localeconv(void)
Definition locale.c:32