/* ** locale.h */ constant int LC_ALL; constant int LC_COLLATE; constant int LC_CTYPE; constant int LC_NUMERIC; constant int LC_TIME; constant int LC_MONETARY; /* lcl can't handle just struct lconv... */ typedef struct lconv { char *decimal_point ; char *thousands_sep ; char *grouping ; char *int_curr_symbol ; char *currency_symbol ; char *mon_decimal_point ; char *mon_thousands_sep ; char *mon_grouping ; char *positive_sign ; char *negative_sign ; char int_frac_digits ; char frac_digits ; char p_cs_precedes ; char p_sep_by_space ; char n_cs_precedes ; char n_sep_by_space ; char p_sign_posn ; char n_sign_posn ; } __lconv ; struct lconv *localeconv(void) { ensures true; } char *etlocale(int __category, char *__locale ) { ensures true; }