¿memcpy(&a + 1, &b + 1, 0) está definido en C11?

Esta pregunta sigue a esta pregunta anterior sobre la definición de memcpy(0, 0, 0), que se ha determinado concluyentemente que es un comportamiento indefinido.

Como muestra la pregunta vinculada, la respuesta depende del contenido de la cláusula 7.1.4:1 de C11

Cada una de las siguientes instrucciones se aplica a menos que se indique explícitamente lo contrario en las descripciones detalladas que siguen: Si un argumento a una función tiene un valor no válido (como un valor fuera del dominio del función, o un puntero fuera del espacio de direcciones del programa, o un puntero nulo, []]) [the] el comportamiento es indefinido. […]

La función estándar memcpy() espera punteros a void y const void, así:

void *memcpy(void * restrict s1, const void * restrict s2, size_t n);

La pregunta vale la pena hacerse en absoluto solo porque hay dos nociones de punteros "válidos" en el estándar: hay punteros que pueden obtenerse válidamente a través de la aritmética de punteros y pueden compararse válidamente con <, > a otros punteros dentro el mismo objeto. Y hay punteros que son válidos para desreferenciar. La primera clase incluye punteros "one-past" como &a + 1 y &b + 1 en el siguiente fragmento, mientras que la segunda clase no los incluye como válidos.

char a;
const char b = '7';
memcpy(&a + 1, &b + 1, 0);

Si el fragmento anterior se considera un comportamiento definido, a la luz del hecho de que los argumentos de memcpy() se escriben como punteros a void de todos modos, por lo que la cuestión de sus respectivas valididades no puede ser sobre desreferenciarlos. O debería &a + 1 y &b + 1 ser considerado "fuera del espacio de direcciones del programa"?

_{Esto me importa porque estoy en el proceso de formalizar los efectos de las funciones C estándar. Había escrito una condición previa de memcpy() como requires \valid(s1+(0 .. n-1));, hasta que se me señaló que GCC 4.9 había comenzado a agresivamenteoptimizar tales llamadas a funciones de biblioteca más allá de lo expresado en la fórmula anterior ( de hecho). La fórmula \valid(s1+(0 .. n-1)) en este lenguaje de especificación particular es equivalente a true cuando n es 0, y no captura el comportamiento indefinido en el que se basa GCC 4.9 para optimizar.}