Parse Java files with unknown library methods

[wadoon]

This issue was created at git.key-project.org where the discussions are preserved.

---

Description

The story is well-known (see #491) and a solution exists but I think there could be a better solution. If this turns out to be completely unfeasible, we can of course close this issue.

As usual, you want to prove something but you can't parse the Java sources, since there is a method call to some (external/core) library. And the method signature is not present. However, you don't really need a contract or the implementation as the present proof obligation does not depend on this method call.

Example

SimpleMin.java

public class SimpleMin {

    /*@ public normal_behavior
          requires true;
          ensures a >= b ==> \result == b;
          ensures a <  b ==> \result == a;
      (at)*/
    public static int min(int a, int b) {
        int m = a;
        if (b < m) m = b;
        a = b = 0;
        return m;
    }

    public static void main (String args[]) {
        int a = 3;
        int b = 7;
        System.out.printf("%d = min(%d, %d)\n", min(a,b), a, b);
    }
}

Status Quo

You could either comment out every such method call (in the example to System.out.printf) or provide add a method stub in a \classpath.

Suggestion

Automatically infer a method signature from the method call (in the example Top printf(String, int, int, int)). Then there is still no contract or implementation but we would be able to parse the sources without issues. Only later, if the symbolic execution reaches such a method, we would get stuck in the proof.

---

Information:

• created_at: 2022-01-06T18:22:25.637Z
• updated_at: 2022-01-11T17:28:43.177Z
• closed_at: None (closed_by: )
• milestone:
• user_notes_count: 5