prusti-dev
prusti-dev copied to clipboard
`extern_spec` panic with `pub` attribute
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.