What the C standard says about extern const

Question

Consider the following program

extern const int foo;
extern void blah(void);

int toto(void) {
  int x = foo;
  blah();
  int y = foo;
  return x + y;
}

arm-linux-gnueabihf-gcc -std=c99 -O2 -fno-pic -S extern_const2.c compiles it to

toto:
    @ args = 0, pretend = 0, frame = 0
    @ frame_needed = 0, uses_anonymous_args = 0
    movw    r3, #:lower16:foo
    movt    r3, #:upper16:foo
    push    {r4, lr}
    ldr r4, [r3]
    bl  blah
    lsls    r0, r4, #1
    pop {r4, pc}

Notice that foo is read once then shifted left by 1, which means that gcc assumes its value to remain constant across the function calls. Similar behavior is observed of clang.

I don't see which part of the ISO/IEC 9899:2017 standard clearly discusses this assumption. §6.7.3-12 explains what to assume about aextern volatile const variable (its value can be changed by hardware, but not be assigned to by the program), but this does not apply to extern const.

§6.7.3-6 states that the program may not assign to a const variable. It is not so clear to me that it implies that an external call cannot mutate this variable.

In addition, the meaning of §6.7.3-6 is not so clear to me. It says

If an attempt is made to modify an object defined with a const-qualified type through use of an lvalue with non-const-qualified type, the behavior is undefined

However, here in my example I declared, not defined, foo as const. The difference between declaration and definition is given in §6.7-5:

A declaration specifies the interpretation and attributes of a set of identifiers. A definition of an identifier is a declaration for that identifier that: — for an object, causes storage to be reserved for that object;

Answer 1

However, here in my example I declared, not defined, foo as const. The difference between declaration and definition is given in §6.7-5:…

The compiler may assume an object declared as const is also defined as const, per C 2018 6.2.7 2:

All declarations that refer to the same object or function shall have compatible type; otherwise, the behavior is undefined.

and 6.7.3 11:

For two qualified types to be compatible, both shall have the identically qualified version of a compatible type; the order of type qualifiers within a list of specifiers or qualifiers does not affect the specified type.

(Note that that sentence does not say what the requirement is for an unqualified type to be compatible with a qualified type, unless we include “no qualifiers” as a qualified type. However, the rules for compatibility are stated throughout the C standard on an affirmative basis: Two types are compatible only if there is a rule stating they are; any types without a statement asserting they are compatible are not compatible.)

§6.7.3-6 states that the program may not assign to a const variable. It is not so clear to me that it implies that an external call cannot mutate this variable.

Per the above, the compiler may assume that foo is const throughout the program and that nothing in the program changes it. If something outside the program could change it, it should be declared volatile.