Skip to content

Verus panics on assume_specification for trait function in same module #2798

Description

@jaylorch

The following code causes Verus to panic:

use vstd::prelude::*;

verus! {

pub struct MyInteger
{
    x: i32
}

impl View for MyInteger
{
    type V = int;

    open spec fn view(&self) -> int
    {
        self.x as int
    }
}

pub assume_specification[ <MyInteger as core::convert::From<i16>>::from ](i: i16) -> (res: MyInteger)
    ensures
        res@ == i,
;

impl core::convert::From<i16> for MyInteger
{
    fn from(i: i16) -> MyInteger
    {
        MyInteger{ x: i as i32 }
    }
}

}

fn main() {
    println!("Hello, world!");
}

This is the panic message:

thread 'rustc' (69533) panicked at vir/src/traits.rs:586:13:
assertion failed: !method_impls.contains(&p)

Metadata

Metadata

Assignees

Labels

No labels
No labels

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions