CBMC
Loading...
Searching...
No Matches
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
}
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
src
ansi-c
library
locale.c
Generated by
1.9.8