Specifications on implementation of the `Drop` trait are not checked

[Pointerbender]

Consider the following Rust program:

use prusti_contracts::*;

fn main() {
    let a = A;
}

pub struct A;

#[refine_trait_spec]
impl Drop for A {
    #[requires(false)]
    fn drop(&mut self) {}
}

This program is successfully verified by Prusti. However, it should not verify, because when a is dropped it should verify this against the precondition #[requires(false)] on <A as Drop>::drop, which should fail verification.

In the generated Viper program for fn main there is no logic related to drop. In the generated MIR there is a drop call to be found in the terminator of the first basic block:

[fpoli]

Thanks for opening the issue. Drop calls are not supported and not verified by Prusti, because we don't get from the unoptimized MIR the precise condition under which the drop call happens. However, we could still at least check the precondition.

[fpoli]

In particular, drop(..) terminators are transformed into method calls and other statements by this MIR pass, which happens after Prusti gets its version of MIR from the compiler.