Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Assignable does not work correctly with Boxed types #3364

Open
fab918 opened this issue Nov 28, 2023 · 0 comments
Open

Assignable does not work correctly with Boxed types #3364

fab918 opened this issue Nov 28, 2023 · 0 comments

Comments

@fab918
Copy link

fab918 commented Nov 28, 2023

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.

@mi-ki mi-ki added the HacKeYthon Candidate Issue for HacKeYthon '24 label Jan 25, 2024
@wadoon wadoon removed the HacKeYthon Candidate Issue for HacKeYthon '24 label Jan 26, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

3 participants