Skip to content

Support deriving kani::Invariant for enums #3647

@carolynzech

Description

@carolynzech

Requested feature: Update the derive macro for the kani::Invariant trait to incorporate the comments from #87 -- i.e., deleting the comments in trivial_invariant about floating point values and supporting enums for the derive macro.

Use case: derive kani::Invariant on enums.

Test case:

#[derive(kani::Invariant)]
enum MyEnum {
    OptionOne(u32, u32),
    OptionTwo(u32),
    OptionThree
}

currently produces

error: proc-macro derive panicked
 --> src/lib.rs:7:10
  |
7 | #[derive(kani::Invariant)]
  |          ^^^^^^^^^^^^^^^
  |
  = help: message: internal error: entered unreachable code

because we have unreachable!() statements for enums and unions in the derive macro implementation.

Metadata

Metadata

Assignees

No one assigned

    Labels

    Z-ContractsIssue related to code contracts[C] Feature / EnhancementA new feature request or enhancement to an existing feature.

    Projects

    No projects

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions