c-semantics

c-semantics copied to clipboard

It would appear the C semantics does not correctly handle inline definitions, but instead treats them as if they are external definitions, which they are not. It would be good for us to fix this case. Cf C11 section 6.7.4.

For example, this program:

inline int foo() { return 6; }

int main() {
  return foo();
}

Should fail to compile because an inline definition was created for the function foo with external linkage, and the identifier was referenced, but it was not given an external definition in another translation unit. However, kcc compiles it successfully.

Similarly, if the following file is compiled into the same program as the previous file:

int foo() { return 6; }

It should then compile successfully because the external definition was used. However, instead, it fails because it believes there are multiple external definitions for foo, even though one is actually an inline definition and therefore not an external definition.

Note: since it is unspecified whether an inline definition or a external definition is used in any particular case, the semantics should make a nondeterministic choice between the two each time the function is called, so that a verifier for C is forced to prove both paths.