CROSSINGTUD / SPDS

Efficient and Precise Pointer-Tracking Data-Flow Framework
Eclipse Public License 2.0
41 stars 37 forks source link

Index +1 shift in Strong Update #53

Closed johspaeth closed 5 years ago

johspaeth commented 6 years ago

The analysis requires intermediate statements before end of branches see class StackTest.

@Test
public void test6() {
    ArrayList l = new ArrayList();
    Stack s = new Stack();
    if (staticallyUnknown()) {
        s.push(new Object());
        int x = 1;
    }
    if (staticallyUnknown()) {
        s.push(new Object());           
        int x = 1;
    }
    if(!s.isEmpty()) {
        Object pop = s.pop();
        mayBeInErrorState(s);
    }
}

The analysis is unsound when we remove the statements x = 1.