How to get the real name of the controlling terminal?

How can one get the real name of the controlling terminal (if there is one, else an error) as a pathname?

By "real name", I mean not /dev/tty, which cannot be used by other arbitrary processes to refer to the same terminal. I prefer the answer as a simple shell code (like the example below) if possible, otherwise as a C function.

Note that this must work even if the standard input is redirected, so that the tty utility cannot be used: one would get a not a tty error in such a case, since tty just prints the file name of the terminal connected to standard input.

Under Linux, one can use:

echo "/dev/`ps -p $$ -o tty | tail -n 1`"

but this is not portable, as according to POSIX, the format of the terminal name is unspecified.

Concerning C functions, ctermid (NULL) returns /dev/tty, which is useless here.