From 7ed21a1b1a2a5471aacaeeb36fa305e67cc24833 Mon Sep 17 00:00:00 2001
From: "Brian R. Murphy" <132495859+brmataptos@users.noreply.github.com>
Date: Mon, 17 Jun 2024 18:48:43 -0700
Subject: [PATCH] Revert "turn 'unresolved spec target' error into a warning
 unless is_verification and keep_testing_functions"

This reverts commit 355e14e306cb081066fe841f2b0d48a11d221833.
---
 .../move-model/src/builder/module_builder.rs  | 11 +-------
 third_party/move/move-model/src/lib.rs        |  2 --
 third_party/move/move-model/src/model.rs      | 26 -------------------
 3 files changed, 1 insertion(+), 38 deletions(-)

diff --git a/third_party/move/move-model/src/builder/module_builder.rs b/third_party/move/move-model/src/builder/module_builder.rs
index e9140f8d2dd1f..a934b63aa7924 100644
--- a/third_party/move/move-model/src/builder/module_builder.rs
+++ b/third_party/move/move-model/src/builder/module_builder.rs
@@ -941,16 +941,7 @@ impl<'env, 'translator> ModuleBuilder<'env, 'translator> {
                 },
                 None => {
                     let loc = self.parent.to_loc(&spec.value.target.loc);
-                    if self.parent.env.is_verification() && self.parent.env.keep_testing_functions()
-                    {
-                        // Only error out on an unknown spec target if we could not
-                        // have elided any as `#[test_only]` or `#[verify_only]`.
-                        self.parent.error(&loc, "unresolved spec target");
-                    } else {
-                        self.parent
-                            .env
-                            .diag(Severity::Warning, &loc, "unresolved spec target");
-                    }
+                    self.parent.error(&loc, "unresolved spec target");
                 },
             }
         }
diff --git a/third_party/move/move-model/src/lib.rs b/third_party/move/move-model/src/lib.rs
index 030a7f59838fb..d6d795ca5f67d 100644
--- a/third_party/move/move-model/src/lib.rs
+++ b/third_party/move/move-model/src/lib.rs
@@ -167,8 +167,6 @@ pub fn run_model_builder_with_options_and_compilation_flags<
     env.set_language_version(options.language_version);
     let compile_via_model = options.compile_via_model;
     env.set_extension(options);
-    env.set_is_verification(flags.is_verification());
-    env.set_keep_testing_functions(flags.keep_testing_functions());
 
     let move_sources = move_sources_targets
         .iter()
diff --git a/third_party/move/move-model/src/model.rs b/third_party/move/move-model/src/model.rs
index 6285cef3f7f18..eb485ab3cd5ee 100644
--- a/third_party/move/move-model/src/model.rs
+++ b/third_party/move/move-model/src/model.rs
@@ -582,10 +582,6 @@ pub struct GlobalEnv {
     /// Whether the v2 compiler has generated this model.
     /// TODO: replace with a proper version number once we have this in file format
     pub(crate) generated_by_v2: bool,
-    /// Whether verification is happening.
-    pub(crate) is_verification: bool,
-    /// Whether we are keeping testing functions.
-    pub(crate) keep_testing_functions: bool,
 }
 
 /// A helper type for implementing fmt::Display depending on GlobalEnv
@@ -647,8 +643,6 @@ impl GlobalEnv {
             address_alias_map: Default::default(),
             everything_is_target: Default::default(),
             generated_by_v2: false,
-            is_verification: false,
-            keep_testing_functions: false,
         }
     }
 
@@ -662,26 +656,6 @@ impl GlobalEnv {
         self.generated_by_v2
     }
 
-    /// Sets whether this is being used for verification.
-    pub fn set_is_verification(&mut self, yes: bool) {
-        self.is_verification = yes
-    }
-
-    /// Returns true if this is being used for verification.
-    pub fn is_verification(&self) -> bool {
-        self.is_verification
-    }
-
-    /// Sets whether we are keeping testing functions.
-    pub fn set_keep_testing_functions(&mut self, yes: bool) {
-        self.keep_testing_functions = yes
-    }
-
-    /// Returns true if we are keeping testing functions.
-    pub fn keep_testing_functions(&self) -> bool {
-        self.keep_testing_functions
-    }
-
     /// Sets the language version.
     pub fn set_language_version(&mut self, version: LanguageVersion) {
         self.language_version = version