viperproject / prusti-dev

A static verifier for Rust, based on the Viper verification infrastructure.
http://prusti.org
Other
1.52k stars 102 forks source link

Enum: unsupported statement kind `Intrinsic(Assume(move _))` #1513

Open nishanthkarthik opened 2 months ago

nishanthkarthik commented 2 months ago

The cast from an enum to its repr triggers this error.

use prusti_contracts::*;

#[derive(Copy, Clone)]
#[repr(u32)]
enum T {
    A = 1,
    B = 2,
}

impl T {
    #[ensures(*self as u32 == result)]
    fn whoami(&self) -> u32 {
        *self as u32
    }
}

Follows from the example in #1512