/* ** ctype.h */ | int : bool | isalnum (| int : char | c ) { ensures true; } | int : bool | isalpha (| int : char | c ) { ensures true; } | int : bool | isascii (| int : char | c ) { ensures true; } | int : bool | iscntrl (| int : char | c ) { ensures true; } | int : bool | isdigit (| int : char | c ) { ensures true; } | int : bool | isgraph (| int : char | c ) { ensures true; } | int : bool | islower (| int : char | c ) { ensures true; } | int : bool | isprint (| int : char | c ) { ensures true; } | int : bool | ispunct (| int : char | c ) { ensures true; } | int : bool | isspace (| int : char | c ) { ensures true; } | int : bool | isupper (| int : char | c ) { ensures true; } | int : bool | isxdigit (| int : char | c ) { ensures true; } | int : char | toascii (| int : char | c ) { ensures true; } | int : char | tolower (| int : char | c ) { ensures true; } | int : char | toupper (| int : char | c ) { ensures true; }