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

Error "Reached assignment statement with unequal types Pointer" with Result<(), Error> #729

Closed
celinval opened this issue Jan 5, 2022 · 1 comment · Fixed by #1205
Closed
Assignees
Labels
[C] Bug This is a bug. Something isn't working. [F] Soundness Kani failed to detect an issue

Comments

@celinval
Copy link
Contributor

celinval commented Jan 5, 2022

I tried this code:

// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
// SPDX-License-Identifier: Apache-2.0 OR MIT

enum Error {
    Error1,
    Error2,
}

fn to_option<T: Copy, E>(result: &Result<T, E>) -> Option<T> {
    if let Ok(v) = result {
        Some(*v)
    } else {
        None
    }
}

fn main() {
    let result: Result<(), Error> = Ok(());
    assert!(to_option(&result).is_some());
}

using the following command line invocation:

rmc <test_file>

with RMC version:

I expected to see this happen: Verification should succeed

Instead, this happened:

$ rmc fixme_niche_opt.rs | grep FAIL
(standard input):34:[assertion.1] Reached assignment statement with unequal types Pointer { typ: StructTag("tag-Unit") } Pointer { typ: StructTag("tag-_3943305294634710273") }: FAILURE
(standard input):66:VERIFICATION FAILED
@celinval celinval added the [C] Bug This is a bug. Something isn't working. label Jan 5, 2022
@celinval
Copy link
Contributor Author

celinval commented Jan 5, 2022

This may be related to #95.

celinval added a commit to celinval/kani-dev that referenced this issue Jan 5, 2022
@danielsn danielsn self-assigned this Jan 6, 2022
celinval added a commit that referenced this issue Jan 6, 2022
Add a fixme testcase that can be used to reproduce the issue #729.
@celinval celinval self-assigned this Mar 14, 2022
@celinval celinval added [F] Soundness Kani failed to detect an issue Status: Mitigated and removed Soundness: Medium labels Apr 20, 2022
tedinski pushed a commit to tedinski/rmc that referenced this issue Apr 22, 2022
Add a fixme testcase that can be used to reproduce the issue model-checking#729.
tedinski pushed a commit to tedinski/rmc that referenced this issue Apr 25, 2022
Add a fixme testcase that can be used to reproduce the issue model-checking#729.
tedinski pushed a commit to tedinski/rmc that referenced this issue Apr 26, 2022
Add a fixme testcase that can be used to reproduce the issue model-checking#729.
tedinski pushed a commit that referenced this issue Apr 27, 2022
Add a fixme testcase that can be used to reproduce the issue #729.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
[C] Bug This is a bug. Something isn't working. [F] Soundness Kani failed to detect an issue
Projects
None yet
Development

Successfully merging a pull request may close this issue.

3 participants