From f6c4ba4f2eed1ca378e2e9801a08df5ed8915dca Mon Sep 17 00:00:00 2001 From: ouz-a Date: Thu, 16 Nov 2023 22:26:19 +0300 Subject: [PATCH] Make codegen_span stable --- .../src/codegen_cprover_gotoc/codegen/span.rs | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs index 27f47ed457c9..9f88bbbe7b55 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs @@ -3,16 +3,21 @@ //! MIR Span related functions -use crate::{codegen_cprover_gotoc::GotocCtx, kani_middle::SourceLocation}; +use crate::codegen_cprover_gotoc::GotocCtx; use cbmc::goto_program::Location; use rustc_middle::mir::{Local, VarDebugInfo, VarDebugInfoContents}; +use rustc_smir::rustc_internal; use rustc_span::Span; impl<'tcx> GotocCtx<'tcx> { pub fn codegen_span(&self, sp: &Span) -> Location { - let loc = SourceLocation::new(self.tcx, sp); + self.stable_codegen_span(&rustc_internal::stable(sp)) + } + + pub fn stable_codegen_span(&self, sp: &stable_mir::ty::Span) -> Location { + let loc = sp.get_lines(); Location::new( - loc.filename, + sp.get_filename().to_string(), self.current_fn.as_ref().map(|x| x.readable_name().to_string()), loc.start_line, Some(loc.start_col),