Wrong linkage of global variables annotated with __attribute__((section))

[cesaro]

Global variables annotated with __attribute__((section ("foo"))), declared in one .c file, and used in a different .c file, are incorrectly linked, leading to wrong verification results.

Using latest develop, in Linux, run

cbmc main.c other.c

where main.c is

#include <assert.h>
#include "other.h"

int main() {

  p.x = 123;

  // valid assertion, gets proof
  assert (p.x == 123);

  int i = get();

  // valid assertion, but gets cex
  assert (i == 123);

  return 0;
}

and other.c is

#include "other.h"

struct point p __attribute__((section ("foo")));

int get () {
  return p.x;
}

and other.h is

#ifndef OTHER_H
#define OTHER_H

struct point {
  int x;
  int y;
};

extern struct point p;

int get ();

#endif

The two assertions are valid. Running the binary generated by gcc doesn't report any assertion violation. But CBMC reports a counterexample for the 2nd assertion.

The problem is visible in the goto functions. References to p.x in main use symbol p, but references to p.x in get and __CPROVER_initialize use foo$$p. CBMC reports the 2nd assertion as valid if the __attribute__ is also added in other.h.