Spans of quantified variables

[fpoli]

The Spanned::get_spans method needs a MIR body to obtain the spans of variables stored in the ForAllVars<'tcx> type. Currently, the MIR body is passed as argument and is used to resolve all quantifiers in an assertion, but each quantifier should use its own MIR body: the one in which the quantified variables are declared.

prusti-dev/prusti-interface/src/specs/typed.rs

Lines 54 to 62 in 7ac30e8

	/// This trait is implemented for specification-related types that have one or
	/// more associated spans (positions within the source code). The spans are not
	/// necessarily contiguous, and may be used for diagnostic reporting.
	pub trait Spanned<'tcx> {
	/// Returns the spans for the given value. `mir` is the function body used
	/// to resolve positions of `rustc_middle::mir::Local` indices, `tcx` is
	/// used to resolve positions of global items.
	fn get_spans(&self, mir_body: &mir::Body<'tcx>, tcx: TyCtxt<'tcx>) -> Vec<Span>;
	}

A solution:

1. Add a definition: LocalDefId field to the typed::ForAllVars structure (this probably requires adding one more type parameter to common::ForAllVars`).
2. Remove the mir_body: mir::Body argument from all Spanned::get_spans methods, using the precedently added definition field to resolve local variables in typed::ForAllVars.

[Aurel300]

Spanned no longer exists in the codebase. Errors (parse and type) are reported at the correct location thanks to how the new preparser works. There are two potential problems still:

• unused qvars are not reported (because somewhere there is an allow(unused_vars) to suppress other warnings we would get, I imagine)
• Prusti encoding/internal errors when encoding a qvar type are unwrapped, or reported with the body span in Small fixes #882

We should get the span of the qvar local from the MIR to report errors (make this change as part of #882).