prusti-dev icon indicating copy to clipboard operation
prusti-dev copied to clipboard

`extern_spec` panic with `pub` attribute

Open Patrick-6 opened this issue 2 years ago • 0 comments

The extern_spec attribute seems to panic on this code example:

use prusti_contracts::*;

#[extern_spec] // <== error shown here
pub trait Clone: Sized {
    #[ensures(self === &result)]
    pub fn clone(&self) -> Self;
}

Error message:

custom attribute panicked
extern_spec_panic.rs(7, 1): message: not implemented: Unimplemented trait item for extern spec

It looks like the pub for the trait and the clone method are not needed, after removing both there are no more errors from Prusti:

use prusti_contracts::*;

#[extern_spec]
trait Clone: Sized {
    #[ensures(self === &result)]
    fn clone(&self) -> Self;
}

There should probably be an error message about removing the pub, or Prusti could also accept the extern_spec if there is a pub.

Patrick-6 avatar Mar 08 '23 13:03 Patrick-6