From bffa0795ca3348deaba90a29e78142148666fc27 Mon Sep 17 00:00:00 2001 From: Andre Maroneze <andre.oliveiramaroneze@cea.fr> Date: Tue, 6 Aug 2019 08:47:27 +0200 Subject: [PATCH] [Libc] fix normalization of __fc prefixes --- share/libc/locale.h | 12 ++++++------ share/libc/syslog.h | 2 +- 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/share/libc/locale.h b/share/libc/locale.h index 11f0244bcb3..6cc0e08923d 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 937e3fcfbe3..107ccb5fd34 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; -- GitLab