char toupper(char c) in { assert(c <= 0x7F); } out (result) { assert(!islower(result)); assert(result <= 0x7F); } body { ... }