search

KeYProject / key

KeY Theorem Prover for Deductive Java Verification
https://key-project.org
Other
41 stars 24 forks source link

Assignable does not work correctly with Boxed types #3364

Open fab918 opened 9 months ago

fab918 commented 9 months ago

Description

I was testing other basic cases and came across this problem, I didn't seem to find any issue that had already been reported.

@ assignable \nothing; should allow modification of a Boxed Type passed in parameter of a method.

Steps to reproduce

    //@ ensures \result == 4;
    //@ assignable \nothing;
    public int computeA(Integer a) {
        a = 4; // OK a is passed by value
        return a;
    }

What is your expected behavior and what was the actual behavior?

The proof doesn't succeed but it should work because, like String, Boxed types are immutable.