The analysis state is not updating correctly

[giacomozanatta]

public class B {
    int i;
    int x;
    C c;
    public B() {
        C c1 = new C();
        this.c = c1;
        this.i = 10;
    }

    public B(int x) {
        this();
        C c1 = new C(x);
        this.c = c1;
        this.x = x;
    }
}

public class C {
    int a;
    public C() {
        this(1000);
    }

    public C(int a) {
        this.a = a;
    }
}

public class Main {
    public static void main(String[] args) {
        B b1 = new B(8);
        B b3 = new B(9);
        //B b2 = new B(100);
        //C c1 = new C();
        //C c3 = new C();
        //C c2 = new C(88);
        //int a = b1.c.a;
    }
}

Analysis Result:

We expect that heap[w]:pp@'B.java':6:15[a]: [8, 9]

[VincenzoArceri]

@giacomozanatta can you please rerun the analysis on this program in the development branch and see if it is fixed now?

[giacomozanatta]

@VincenzoArceri the result now is different:

heap[w]:pp@'B.java':13:15[a]: [0, 9]

The location and the interval changed.

[VincenzoArceri]

is it correct?

[giacomozanatta]

If by correct you mean sound, then yes, the result is correct, but it is over-approximated.
This is the trace restricted to the variable a:

Main {
b1 = B(8) -> heap[s]:pp@'B.java':13:15[a]: [8, 8]
b3 = B(9) {
B(this) -> heap[s]:pp@'B.java':13:15[a]: [8, 8]
c1 = C(9) {
C() -> heap[w]:pp@'B.java':13:15[a]: [8, 8]
this.a = 0 -> heap[w]:pp@'B.java':13:15[a]: [0, 8] // losing precision due to the weak access.
this.a = 9 -> heap[w]:pp@'B.java':13:15[a]: [0, 9]
}
...
}
...
} -> heap[w]:pp@'B.java':13:15[a]: [0, 9]

Can we improve this? I think yes, but the loss of precision is probably due to how LiSA handles weak accesses.

[VincenzoArceri]

I think that better than that, with the FieldSensitivePointBasedHeap analysis, we cannot do (but please @lucaneg double-check it). I think we could create a kind of 'allocation-site' based on something like 'call-string' rather than the precise location, but I think we do not need it for SVComp (let's leave it for future work)

[lucaneg]

I don't understand where the 0 comes from: the zero init should happen only if there is no assignment to field a. So the interval should be [8,9] instead of [0,9]. Apart from this, then yes, the program point based analysis does not distinguish between different objects allocated at the sime place in the source code. It does not matter if they are allocated at different loop iterations or if the allocations is reached with different call stacks. We need a separate analysis for that, but you would still need some form of summarization to ensure convergence, leading to the same situation here (even if less often).