annotations: calculus refactoring

moves-rwth · Jan 16, 2024 · ad861f3 · ad861f3
1 parent a286130
commit ad861f3
Show file tree

Hide file tree

Showing 16 changed files with 321 additions and 481 deletions.
diff --git a/src/calculi/ert.rs b/src/calculi/ert.rs
diff --git a/src/calculi/mod.rs b/src/calculi/mod.rs
diff --git a/src/calculi/tests.rs b/src/calculi/tests.rs
diff --git a/src/calculi/wlp.rs b/src/calculi/wlp.rs
diff --git a/src/calculi/wp.rs b/src/calculi/wp.rs
diff --git a/src/driver.rs b/src/driver.rs
@@ -10,7 +10,6 @@ use crate::{
         visit::VisitorMut, Block, DeclKind, Expr, ExprData, ExprKind, LitKind, Shared,
         SourceFilePath, Span, Spanned, StoredFile, TyKind,
     },
-    calculi::CalculusVisitor,
     front::parser,
     front::resolve::{Resolve, ResolveError},
     front::{
@@ -190,17 +189,6 @@ impl SourceUnit {
         }
     }
 
-    #[instrument(skip(self, tcx))]
-    pub fn check_calculus(&mut self, tcx: &mut TyCtx) -> Result<(), AnnotationError> {
-        let mut calculus_visitor = CalculusVisitor::new(tcx);
-
-        match self {
-            SourceUnit::Decl(decl) => calculus_visitor.visit_decl(decl),
-            // Not supported for raw source units since calculus annotations are only allowed on procedures
-            SourceUnit::Raw(_) => Ok(()),
-        }
-    }
-
     /// Return a new [`Item`] by wrapping it around the [`SourceUnit`]
     /// and set the file path of the new [`SourceUnitName`] to the given file_path argument
     /// This function is used to generate [`Item`]s from generated [`SourceUnit`] objects (through AST transformations)