Overloading of methods in java depends on ordering

[bobismijnnaam]

The following input:

class C {
    //@ requires 1 == 2;
    void foo(float x) {

    }

    void foo(int x) {

    }

    void bar() {
        foo(2);
    }
}

Yields:

[INFO] Starting verification
======================================
 At xx.java.bak:12:9:
--------------------------------------
   10  
   11      void bar() {
              [------
   12          foo(2);
               ------]
   13      }
   14  }
--------------------------------------
[1/2] Precondition may not hold, since ...
--------------------------------------
 At xx.java.bak:2:18:
--------------------------------------
    1  class C {
                       [------
    2      //@ requires 1 == 2;
                        ------]
    3      void foo(float x) {
    4  
--------------------------------------
[2/2] ... this expression may be false (https://utwente.nl/vercors#preFailed:false)
======================================
======================================
At xx.java.bak:3:5:
--------------------------------------
    1  class C {
    2      //@ requires 1 == 2;
          [---------------------
    3      void foo(float x) {
    4  
    5      }
       -----]
    6  
    7      void foo(int x) {
--------------------------------------
The precondition of this contract may be unsatisfiable. If this is intentional, replace it with `requires false`. (https://utwente.nl/vercors#unsatisfiable)
======================================

I would expect it to pass (besides the unsat error, that's expected), since the type of 2 is int. I guess I either made a mistake when implementing floats or the overloading resolving system was order-dependent to begin with.

[Ellen-Wittingen]

Overloading seems order-dependent indeed, at least in the implementation for C. In the example below it verifies successfully even though the postcondition of main() should be false. If the postcondition of main() is changed to \result == 6 it does not verify. It does seem to know that incr(int a) exists, otherwise I would expect an error in the body of main(), but for verifying it seems to grab the contract of the first method with the correct name without taking parameters into account.

//@ ensures \result == 5;
int incr() {
  return 5;
}

//@ ensures \result == 6;
int incr(int a) {
  return 6;
}

//@ ensures \result == 5;
int main() {
  return incr(7);
}

[pieter-bos]

VerCors generally assumes that the example compiles. In the case of C programs, it is not legal to redefine declarations in C, so for C VerCors just takes the first declaration that is named correctly. As you may know there is no concept of overloading in C, so the resolution does not account for selecting a declaration with the correct shape of arguments. It seems that the error you are expecting is unfortunately missing, there should be a structural check that the number of given arguments matches the declaration. It seems the argument is silently dropped somewhere in the rewrite chain.

Bob's example is written in Java, where we do consider overloading and the shape of the arguments. It appears that there is a type rule that coerces integers into (our current flawed interpretation of) floats. This should be resolved by any concerted effort to improve our support for floats :)