Interference of fields of structures in arrays

[tomsik68]

Run symbiotic --32 --prp memsafety --no-slice rc.c with symbiotic 5f6b411 Where rc.c is the following:

// simple reference counter
typedef struct {
    void *obj;
    int count;
} rc_t;

static rc_t rcs[1];
static int rc_count = 0;

int main(int argc, char *argv[])
{
    int x = 42;

    // initialize rc with a valid pointer to x=42
    rcs[rc_count].obj = &x;
    // now initialize count to 0
    rcs[rc_count].count = 0;

    // get back the object (x)
    int *dr = (int *) rcs[rc_count].obj;

    // try to access the object
    __VERIFIER_assert(*dr == 42);

    return 0;
}

Symbiotic reports there is an invalid dereference on the __VERIFIER_assert line, while the program has no issues. Deleting rcs[rc_count].count = 0; produces the correct answer again. Swapping order of those two assignments to rcs[rc_count] produces the correct answer aswell.

It looks like rcs[rc_count].count = 0; invalidates the pointer inside of the structure. This issue also occurs with the SV-COMP benchmark https://github.com/sosy-lab/sv-benchmarks/blob/master/c/ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i .