Use interior mutability in translaion contexts instead of passing mut…

…able borrows everywhere.
creusot-rs · Feb 12, 2025 · 63533f6 · 63533f6
1 parent dde8c4c
commit 63533f6
Show file tree

Hide file tree

Showing 30 changed files with 415 additions and 407 deletions.
diff --git a/Cargo.lock b/Cargo.lock
diff --git a/creusot/Cargo.toml b/creusot/Cargo.toml
@@ -22,6 +22,7 @@ tempdir = "0.3"
 serde_json = "1.0"
 lazy_static = "1.5"
 pathdiff = "0.2"
+once_map = "0.4"
 
 [dev-dependencies]
 clap = { version = "4.5", features = ["derive", "env"] }

diff --git a/creusot/src/backend.rs b/creusot/src/backend.rs
@@ -12,6 +12,7 @@ use crate::{
     util::path_of_span,
 };
 use std::{
+    cell::RefCell,
     ops::{Deref, DerefMut},
     path::PathBuf,
 };
@@ -33,9 +34,9 @@ pub(crate) mod ty_inv;
 pub(crate) mod wto;
 
 pub struct Why3Generator<'tcx> {
-    ctx: TranslationCtx<'tcx>,
+    pub ctx: TranslationCtx<'tcx>,
     functions: Vec<TranslatedItem>,
-    pub(crate) span_map: SpanMap,
+    pub(crate) span_map: RefCell<SpanMap>,
 }
 
 impl<'tcx> Deref for Why3Generator<'tcx> {
@@ -96,10 +97,10 @@ impl<'tcx> Why3Generator<'tcx> {
         matches!(self.item_type(item), ItemType::Logic { .. } | ItemType::Predicate { .. })
     }
 
-    pub(crate) fn span_attr(&mut self, span: Span) -> Option<why3::declaration::Attribute> {
+    pub(crate) fn span_attr(&self, span: Span) -> Option<why3::declaration::Attribute> {
         let path = path_of_span(self.tcx, span, &self.opts.span_mode)?;
 
-        if let Some(span) = self.span_map.encode_span(&self.ctx.opts, span) {
+        if let Some(span) = self.span_map.borrow_mut().encode_span(&self.ctx.opts, span) {
             return Some(span);
         };