Difference in verification depending where the static method is place.

[wadoon]

Description

Consider the file Point3d.java. Method Point3d#test() is not verifiable, where as Use#m() is. Content-wise, they are identical.

public record Point3d(int x, int y, int z) {
    /*@ normal_behavior ensures true; requires true; */
    public static void test() {
        Point3d p = new Point3d(1, 2, 3);

        //boolean b= p.equals(p);
        // @assert b;

        //@ assert p.x() == 1;
        //@ assert p.y() == 2;
        //@ assert p.z() == 3;

        //@assert p.equals(p);

        Point3d q = new Point3d(p.x, p.y, p.z);
        //@assert p.equals(q);
        //@assert q.equals(p);
    }
}

class Use {
    /*@ normal_behavior ensures true; requires true; */
    public static void m() {
        Point3d p = new Point3d(1, 2, 3);

        //boolean b= p.equals(p);
        // @assert b;

        //@ assert p.x() == 1;
        //@ assert p.y() == 2;
        //@ assert p.z() == 3;

        //@assert p.equals(p);

        Point3d q = new Point3d(p.x, p.y, p.z);
        //@assert p.equals(q);
        //@assert q.equals(p);
    }
}

Reproducible

always

Steps to reproduce

Describe the steps needed to reproduce the issue.

1. Load the example above.
2. Prove Use#m() using auto
3. Try to prove Point3d#test()

---

• Commit: 4fc5ecc

[WolframPfeifer]

In the example above, both methods are static. Is the title of this PR or the example code wrong?

[WolframPfeifer]

I am confused now: Shouldn't the example be at least loadable after #3905 on the current RC for KeY 3.0? I thought there was a pipeline step that transforms records into normal classes?!

Edit: I got confused with the branches, and tried on prereleases/KeY-3.0.0-JP-rc instead of prereleases/KeY-3.0.0-rc, which is the correct RC branch and on which it loads as expected. Can we delete the former, as it is very easy to confuse?

[WolframPfeifer]

Now that the title is changed: I cannot reproduce this, as I am not able to prove any of the two variants.

[unp1]

The underlying reason is that different query rules are used:

The closing one uses "EvaluateQuery", the open one "Query_Axiom". They differ in how the expand an "self.equals(o)" (self is of sort Point3d) function in the logic. Evaluate query generates
\[ method-frame(source = Point3d) { res = self.equals(o) } \] post
while Query_Axiom... generates
\[ self.equals(o) @ Point3d \] post
without the source context.
Consequently, the one using Evaluate Query can use the equals contract from Point3d and the other cannot do anything as it would need to inline the Point3d implementation, which is not available.

One can close both by switching "Expand local queries" off in the strategy pane and this enforcing the use of Evaluate Query

But both rules are not ok in my opinion as they do not consider the call context in which the query was issued. They use the static type of the caller as substitute. In general, the JML translation needs to pass the class context in which the query is called onwards to the translated function o.m(), which most likely means we need another function symbol o.m()#called-in- and then on expand use as source context for the method frame.

[unp1]

PR #3980 fixes this issue but does not address the broader problem