diff --git a/prusti-interface/src/specs/mod.rs b/prusti-interface/src/specs/mod.rs index 3cccf06ee4b..da3dc160b1c 100644 --- a/prusti-interface/src/specs/mod.rs +++ b/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, diff --git a/prusti-interface/src/specs/typed.rs b/prusti-interface/src/specs/typed.rs index 797e9839941..791b24a2917 100644 --- a/prusti-interface/src/specs/typed.rs +++ b/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 Refinable for SpecificationItem { 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, pub kind: SpecificationItem, pub pres: SpecificationItem>, pub posts: SpecificationItem>, @@ -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, diff --git a/prusti-tests/tests/verify_overflow/fail/extern-spec/trait-impls/traits-2.rs b/prusti-tests/tests/verify_overflow/fail/extern-spec/trait-impls/traits-2.rs index 54b238679b0..b5e8334cfaa 100644 --- a/prusti-tests/tests/verify_overflow/fail/extern-spec/trait-impls/traits-2.rs +++ b/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() { diff --git a/prusti-viper/src/encoder/mir/pure/pure_functions/encoder.rs b/prusti-viper/src/encoder/mir/pure/pure_functions/encoder.rs index 9f1f116c894..c8bd212664a 100644 --- a/prusti-viper/src/encoder/mir/pure/pure_functions/encoder.rs +++ b/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; diff --git a/prusti-viper/src/encoder/mir/pure/pure_functions/new_encoder.rs b/prusti-viper/src/encoder/mir/pure/pure_functions/new_encoder.rs index 3a442cba685..b78146d1445 100644 --- a/prusti-viper/src/encoder/mir/pure/pure_functions/new_encoder.rs +++ b/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; diff --git a/prusti-viper/src/encoder/mir/specifications/interface.rs b/prusti-viper/src/encoder/mir/specifications/interface.rs index 53e4c004f94..7a0edb40393 100644 --- a/prusti-viper/src/encoder/mir/specifications/interface.rs +++ b/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; - /// 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)) + } }