Clarify failing postcondition of trait method

[fpoli]

trafficstars

In the following program Prusti identifies a verification error as expected: the method implementation A::bar does not specify a postcondition, so it gets by default the result > 10 from the trait definition, but the implementation returns 0. The error message currently points to the failing postcondition in the trait definition, but this is ambiguous because there are multiple types that implement that trait, and it's not immediately clear which of them is involved in the error.

The error message should use as primary span the fn baz() -> usize in the method implementation, excluding the method's body { .. } to keep the span short and readable.

extern crate prusti_contracts;

trait Foo {
    #[ensures="result > 10"] // Failing postcondition. The verification error is currently reported here.
    fn bar() -> usize;
}

struct A;

impl Foo for A {
    fn bar() -> usize { // Bad implementation. The verification error should be reported here.
        0
    }
}

struct B;

impl Foo for B {
    fn bar() -> usize { // Correct implementation
        100
    }
}

fn main(){}

[JonasAlaif]

This is still an issue:

use prusti_contracts::*;

trait Foo {
    #[ensures(result > 10)] // Failing postcondition. The verification error is currently reported here.
    fn bar() -> usize;
}

struct A;

impl Foo for A {
    fn bar() -> usize { // Bad implementation. The verification error should be reported here.
        0
    }
}

struct B;

impl Foo for B {
    fn bar() -> usize { // Correct implementation
        100
    }
}

fn main(){}

[Aurel300]

The failing implementation span is now added as a "note" to the error:

error: [Prusti: verification error] postcondition might not hold.
  --> example.rs:4:15
   |
4  |     #[ensures(result > 10)] // Failing postcondition. The verification error is currently reported here.
   |               ^^^^^^^^^^^
   |
note: the error originates here
  --> example.rs:11:5
   |
11 | /     fn bar() -> usize { // Bad implementation. The verification error should be reported here.
12 | |         0
13 | |     }
   | |_____^

Do we want to improve this any further? I think reporting the failing postcondition (or conjunct) as the primary span makes sense.