Inconsistent behavior of string literals between reference interpreter and generated object code

[monniaux]

On x86-64 (possibly on other architectures) the following program returns 1:

int main() {
  const char * const a = "ABBA";
  const char * const b = "BA";
  return (b==a+2);
}

This is due to the use of string literal linker sections that the linker is allowed to merge: if a string is a right substring of another, then it will be merged into the other string. (This is reasonable especially for printf format strings.)

Yet CompCert's interpreter returns 0, as it considers that a and b point to two different string literals, each living in its own block.

This is not a serious issue. Maybe a word of warning in the manual? Or an option for disallowing mergeable linker sections?