remember spans for extern specs

prusti-interface/src/specs/mod.rs

@@ -118,6 +118,7 @@ impl<'a, 'tcx> SpecCollector<'a, 'tcx> {
             def_spec.specs.insert(
                 local_id.to_def_id(),
                 typed::SpecificationSet::Procedure(typed::ProcedureSpecification {
+                    span: Some(self.env.get_def_span(local_id.to_def_id())),
                     pres,
                     posts,
                     pledges,

prusti-interface/src/specs/typed.rs

@@ -4,7 +4,7 @@ use prusti_specs::specifications::common;
 use rustc_hir::def_id::{DefId, LocalDefId};
 use std::{collections::HashMap, fmt::Debug};
 use std::fmt::{Display, Formatter};
-
+use rustc_span::Span;
 
 #[derive(Debug, Clone)]
 pub enum SpecificationSet {
@@ -259,6 +259,7 @@ impl<T: Debug + Clone + PartialEq> Refinable for SpecificationItem<T> {
 impl Refinable for ProcedureSpecification {
     fn refine(self, other: &Self) -> Self {
         ProcedureSpecification {
+            span: self.span.or(other.span),
             pres: self.pres.refine(&other.pres),
             posts: self.posts.refine(&other.posts),
             pledges: self.pledges.refine(&other.pledges),
@@ -282,6 +283,7 @@ impl Refinable for SpecificationSet {
 
 #[derive(Debug, Clone)]
 pub struct ProcedureSpecification {
+    pub span: Option<Span>,
     pub kind: SpecificationItem<ProcedureSpecificationKind>,
     pub pres: SpecificationItem<Vec<LocalDefId>>,
     pub posts: SpecificationItem<Vec<LocalDefId>>,
@@ -292,6 +294,7 @@ pub struct ProcedureSpecification {
 impl ProcedureSpecification {
     pub fn empty() -> Self {
         ProcedureSpecification {
+            span: None,
             kind: SpecificationItem::Empty,
             pres: SpecificationItem::Empty,
             posts: SpecificationItem::Empty,

prusti-tests/tests/verify_overflow/fail/extern-spec/trait-impls/traits-2.rs

@@ -22,7 +22,7 @@ impl Max for Point {
     #[pure]
     #[ensures(result >= self.0 && result >= self.1)]
     #[ensures(result == self.0 || result == self.1)]
-    fn max(&mut self) -> i32;   //~ ERROR: pure function parameters must be Copy
+    fn max(&mut self) -> i32; //~ ERROR: pure function parameters must be Copy
 }
 
 fn main() {

prusti-viper/src/encoder/mir/pure/pure_functions/encoder.rs

@@ -10,6 +10,7 @@ use crate::encoder::{
     errors::{ErrorCtxt, SpannedEncodingError, SpannedEncodingResult, WithSpan},
     high::{generics::HighGenericsEncoderInterface, types::HighTypeEncoderInterface},
     mir::pure::{PureEncodingContext, SpecificationEncoderInterface},
+    mir::specifications::SpecificationsInterface,
     mir_encoder::PlaceEncoder,
     mir_interpreter::run_backward_interpretation,
     snapshot::interface::SnapshotEncoderInterface,
@@ -94,7 +95,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> PureFunctionEncoder<'p, 'v, 'tcx> {
             encoder.env().identity_substs(proc_def_id).len()
         );
 
-        let span = encoder.env().tcx().def_span(proc_def_id);
+        let span = encoder.get_spec_span(proc_def_id);
 
         // TODO: move this to a signatures module
         use crate::rustc_middle::ty::subst::Subst;

prusti-viper/src/encoder/mir/pure/pure_functions/new_encoder.rs

@@ -8,11 +8,13 @@ use crate::encoder::{
             interpreter::ExpressionBackwardInterpreter,
             specifications::SpecificationEncoderInterface,
         },
+        specifications::SpecificationsInterface,
         types::MirTypeEncoderInterface,
     },
     mir_interpreter::run_backward_interpretation,
     Encoder,
 };
+
 use log::{debug, trace};
 use prusti_common::vir_high_local;
 use rustc_hir::def_id::DefId;
@@ -155,7 +157,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> PureEncoder<'p, 'v, 'tcx> {
             encoder.env().identity_substs(proc_def_id).len()
         );
 
-        let span = encoder.env().tcx().def_span(proc_def_id);
+        let span = encoder.get_spec_span(proc_def_id);
 
         // TODO: move this to a signatures module
         use crate::rustc_middle::ty::subst::Subst;

prusti-viper/src/encoder/mir/specifications/interface.rs

@@ -5,6 +5,7 @@ use prusti_interface::{
     utils::has_spec_only_attr,
 };
 use rustc_hir::def_id::{DefId, LocalDefId};
+use rustc_span::Span;
 use std::cell::RefCell;
 
 pub(crate) struct SpecificationsState {
@@ -33,8 +34,12 @@ pub(crate) trait SpecificationsInterface {
     /// Get the specifications attached to the `def_id` function.
     fn get_procedure_specs(&self, def_id: DefId) -> Option<typed::ProcedureSpecification>;
 
-    /// Is the closure specified with the `def_id` is spec only?
+    /// Is the closure specified with the `def_id` spec only?
     fn is_spec_closure(&self, def_id: DefId) -> bool;
+
+    /// Get the span of the declared specification, if any, or else the span of
+    /// the method declaration.
+    fn get_spec_span(&self, def_id: DefId) -> Span;
 }
 
 impl<'v, 'tcx: 'v> SpecificationsInterface for super::super::super::Encoder<'v, 'tcx> {
@@ -88,8 +93,16 @@ impl<'v, 'tcx: 'v> SpecificationsInterface for super::super::super::Encoder<'v,
         Some(spec.clone())
     }
 
-    /// Is the closure specified with the `def_id` is spec only?
     fn is_spec_closure(&self, def_id: DefId) -> bool {
         has_spec_only_attr(self.env().tcx().get_attrs(def_id))
     }
+
+    fn get_spec_span(&self, def_id: DefId) -> Span {
+        self.specifications_state
+            .specs
+            .borrow_mut()
+            .get_and_refine_proc_spec(self.env(), def_id)
+            .and_then(|spec| spec.span)
+            .unwrap_or_else(|| self.env().get_def_span(def_id))
+    }
 }