diff --git a/share/libc/locale.h b/share/libc/locale.h index 11f0244bcb3cf4b8f4df547113ba2de04669bf37..6cc0e08923d1ce49e3075c5195407f7d4ff324c2 100644 --- a/share/libc/locale.h +++ b/share/libc/locale.h @@ -131,20 +131,20 @@ struct lconv | LC_IDENTIFICATION_MASK \ ) -extern struct lconv* __frama_c_locale; -extern char*__frama_c_locale_names[512]; +extern struct lconv* __fc_locale; +extern char*__fc_locale_names[512]; /*@ requires locale_null_or_valid_string: locale == \null || valid_read_string(locale); - assigns __frama_c_locale \from category, locale[..]; - assigns \result \from __frama_c_locale,category, locale[..]; + assigns __fc_locale \from category, locale[..]; + assigns \result \from __fc_locale,category, locale[..]; ensures result_null_or_locale_name: \result==\null || (\valid(\result) - && \exists ℤ i ; \result == __frama_c_locale_names[i]) ; + && \exists ℤ i ; \result == __fc_locale_names[i]) ; */ extern char *setlocale(int category, const char *locale); /*@ assigns \nothing; - ensures result_current_locale: \result == __frama_c_locale; + ensures result_current_locale: \result == __fc_locale; */ extern struct lconv *localeconv(void); diff --git a/share/libc/syslog.h b/share/libc/syslog.h index 937e3fcfbe3a1a9e781946dcc26615d65afade6c..107ccb5fd3471df1cefa5512a76f14f495180b19 100644 --- a/share/libc/syslog.h +++ b/share/libc/syslog.h @@ -29,7 +29,7 @@ __PUSH_FC_STDLIB __BEGIN_DECLS -typedef struct _code { +typedef struct __fc_code { const char *c_name; int c_val; } CODE;