Missing Source Snippets in some circumstances

[juliand665]

This is probably not actually the most general case, but with #1249 there's a simple way to produce this error. The following client code will do it:

struct Special {
    x: i32,
}

impl Clone for Special {
    fn clone(&self) -> Self {
        Special { x: self.x + 1 }
    }
}

This violates the postcondition applied to Clone implementers by default through this spec, i.e. ensures(result === x). One would expect to see an error like this:

However, the produced error is actually missing the source snippet of the spec:

One way I've found to bring back this info is to explicitly use prusti_contracts::core_spec::clone; (or anything within the clone module). I don't know enough about how Prusti handles this stuff to come up with a good theory of what's going on, but maybe this insight will set off a lightbulb for someone who knows their way around :)

[fpoli]

This happened to me today. It's not a full explanation, but I noticed that here we register the span of the function instead of the span of the postcondition:

https://github.com/viperproject/prusti-dev/blob/3dd957cf440edf04504f6b0ca8b57fac64e813a7/prusti-viper/src/encoder/procedure_encoder.rs#L4858-L4866

Usually that span should not matter because Viper should report in the verification error the position of the precise sub-expression in the postcondition that failed. However, if that doesn't happen Prusti will fall-back to the position of the assertion, thus the self.mir.span in the snipped above.