Revert "further cleanup"

This reverts commit 2fa0ace.
MystenLabs · Dec 20, 2024 · 30cd739 · 30cd739
1 parent 2fa0ace
commit 30cd739
Show file tree

Hide file tree

Showing 3 changed files with 30 additions and 5 deletions.
diff --git a/external-crates/move/crates/move-compiler/src/compiled_unit.rs b/external-crates/move/crates/move-compiler/src/compiled_unit.rs
@@ -29,6 +29,13 @@ pub struct VarInfo {
     pub index: F::LocalIndex,
 }
 
+#[derive(Debug, Clone)]
+pub struct SpecInfo {
+    pub offset: F::CodeOffset,
+    // Free locals that are used but not declared in the block
+    pub used_locals: UniqueMap<H::Var, VarInfo>,
+}
+
 #[derive(Debug, Clone)]
 pub struct FunctionInfo {
     pub parameters: Vec<(H::Var, VarInfo)>,

diff --git a/external-crates/move/crates/move-compiler/src/parser/verification_attribute_filter.rs b/external-crates/move/crates/move-compiler/src/parser/verification_attribute_filter.rs
@@ -48,11 +48,9 @@ impl FilterContext for Context<'_> {
     // An AST element should be removed if:
     // * It is annotated #[spec_only] and verify mode is not set
     fn should_remove_by_attributes(&mut self, attrs: &[P::Attributes]) -> bool {
-        // uncomment this condition to disable filtering out specs
-        // if self.env.flags().is_verifying() {
-        //     return false;
-        // }
-
+        if self.env.flags().is_verifying() {
+            return false;
+        }
         use known_attributes::VerificationAttribute;
         let flattened_attrs: Vec<_> = attrs.iter().flat_map(verification_attributes).collect();
         //

diff --git a/external-crates/move/crates/move-compiler/src/shared/mod.rs b/external-crates/move/crates/move-compiler/src/shared/mod.rs
@@ -605,6 +605,13 @@ pub struct Flags {
     )]
     test: bool,
 
+    /// Compile in verify mode
+    #[clap(
+        short = cli::VERIFY_SHORT,
+        long = cli::VERIFY,
+    )]
+    verify: bool,
+
     /// If set, warnings become errors.
     #[clap(
         long = cli::WARNINGS_ARE_ERRORS,
@@ -657,6 +664,7 @@ impl Flags {
     pub fn empty() -> Self {
         Self {
             test: false,
+            verify: false,
             shadow: false,
             bytecode_version: None,
             warnings_are_errors: false,
@@ -671,6 +679,7 @@ impl Flags {
     pub fn testing() -> Self {
         Self {
             test: true,
+            verify: false,
             shadow: false,
             bytecode_version: None,
             warnings_are_errors: false,
@@ -682,6 +691,13 @@ impl Flags {
         }
     }
 
+    pub fn set_verify(self, value: bool) -> Self {
+        Self {
+            verify: value,
+            ..self
+        }
+    }
+
     pub fn set_keep_testing_functions(self, value: bool) -> Self {
         Self {
             keep_testing_functions: value,
@@ -739,6 +755,10 @@ impl Flags {
         self.test
     }
 
+    pub fn is_verifying(&self) -> bool {
+        self.verify
+    }
+
     pub fn keep_testing_functions(&self) -> bool {
         self.test || self.keep_testing_functions
     }