restrict Qualifier in C

Question

Is the following valid usage of restrict qualifier in C or undefined behaviour?

#include <stdio.h>

int foo(float * restrict a) {
    float a1 = *a;
    float a2 = *(a+1);

    float * restrict c = a;
    
    *c = 1;
    *(c+1) = 2;
    
    // are compilers obliged to load a[0] and a[1] again?
    printf("%f %f\n",*a,*(a+1));
    printf("%p %p\n", (void *)a1, (void *)a2);
}

Answer 1

The restrict qualifier of a is not being violated.

The restrict qualifier of a does not disallow to modify the array through c instead of a, because the value of c depends on the value of a. So you are indirectly modifying the array through a, which is permissible as far as the restrict qualifier of a is concerned.

The restrict qualifier of c is being violated.

§6.7.4.2 ¶4 of the ISO C23 standard states the following:

During each execution of B, let L be any lvalue that has &L based on P. If L is used to access the value of the object X that it designates, and X is also modified (by any means), then the following requirements apply: [...] Every other lvalue used to access the value of X shall also have its address based on P.

In that quote,

• B is the block containing the restrict pointer declaration, or the entire function block in the case of a parameter being declared with the restrict qualifier,
• X is the object referenced by the pointer, and
• P is the pointer object itself.

The sentence

Every other lvalue used to access the value of X shall also have its address based on P.

is being violated, because in the line

printf("%f %f\n",*a,*(a+1));

the referenced object X is being accessed through a, and a does not depend on c (c depends on a, but not vice versa).

The terms "depends on" and "based on" are being used by me synonymously. The ISO C23 standard only uses the term "based on", and defines this term in §6.7.4.2 ¶3 the following way:

In what follows, a pointer expression E is said to be based on object P if (at some sequence point in the execution of B prior to the evaluation of E) modifying P to point to a copy of the array object into which it formerly pointed would change the value of E.

Conclusion

Since the restrict qualifier of c is being violated, the posted code has undefined behavior. Had only a been declared with the restrict qualifier and c been declared without that qualifier, then the program's behavior would have been well-defined.

The previous statement is based on the assumption that a points to an array of float with at least two elements. If that is not the case, then the program's behavior would also be undefined in the case specified above.