Skip to content

Assert_eq! hits unreachable code #292

@obriematt

Description

@obriematt

Testing for assert_eq! seems to be hitting unreachable code within weakest_precondition line 80.

It doesn't seem to contain "begin_panic" like our code is expecting.

Current test that doesn't work:

// Should be valid
#[condition(pre="x: i32 == 10i32", post="true")]
fn valid_simple_assertion_eq(x: i32) {
    assert_eq!(x, 10);
}

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type
    No fields configured for issues without a type.

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions