Contract members appear to be interpreted as static and not as instance variables

[fbrausse]

While trying to fix the Solidity issues occurring with #1696, I came across this variation of regression/esbmc-solidity/constructor_4:

// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.5.0;

contract BB {
    uint8 data;

    constructor(uint8 x, uint8 y) {
        data = x + y;
    }

    function empty1() public {
        assert(data == 2);
    }

    function empty(uint8 x, uint256 y) public {
        data = data + x;
        empty1();
    }
}

contract DD {
    BB x = new BB(2, 0);
    BB y = new BB(3, 0); // this line is new, rest unchanged

    function empty2() public {}

    function D() public {
        x.empty(0, 2);
    }
}

Current master says VERIFICATION FAILED with --function D. When removing the new line or moving it above BB x = new BB(2, 0);, it is successfully verified. The reason is that the data member of BB is interpreted as a static instead of instance variable.

As I don't know much about Solidity, could someone confirm whether this is a bug or whether this is indeed the indended behaviour?

This is the corresponding solast file generated with solc version 0.8.24+commit.e11b9ed9.Linux.g++: ctor4-2.solast.txt

[lucasccordeiro]

@ChenfengWei0: could you check this issue?

[ChenfengWei0]

Probably a bug. Might due to the name issue I am trying to fix #1697. Will investigate. Thanks for reporting this, @fbrausse !