Spec Scope Changes

crates/move-model/src/builder/module_builder.rs

@@ -88,6 +88,7 @@ impl<'env, 'translator> ModuleBuilder<'env, 'translator> {
         self.populate_env_from_result(
             loc,
             attributes,
+            module_def.attributes,
             compiled_module,
             source_map,
             &function_infos,
@@ -516,6 +517,7 @@ impl ModuleBuilder<'_, '_> {
         &mut self,
         loc: Loc,
         attributes: Vec<Attribute>,
+        toplevel_attributes: EA::Attributes,
         module: CompiledModule,
         source_map: SourceMap,
         function_infos: &UniqueMap<PA::FunctionName, FunctionInfo>,
@@ -657,6 +659,7 @@ ot in AST",
         self.parent.env.add(
             loc,
             attributes,
+            toplevel_attributes,
             module,
             source_map,
             named_constants,

crates/move-model/src/model.rs

@@ -916,6 +916,7 @@ impl GlobalEnv {
         &mut self,
         loc: Loc,
         attributes: Vec<Attribute>,
+        toplevel_attributes: expansion::ast::Attributes,
         module: CompiledModule,
         source_map: SourceMap,
         named_constants: BTreeMap<NamedConstantId, NamedConstantData>,
@@ -966,6 +967,7 @@ impl GlobalEnv {
             source_map,
             loc,
             attributes,
+            toplevel_attributes,
             used_modules: Default::default(),
             friend_modules: Default::default(),
         });
@@ -3942,6 +3944,7 @@ impl GlobalEnv {
                 ),
                 loc: Loc::default(),
                 attributes: Default::default(),
+                toplevel_attributes: Default::default(),
                 used_modules: Default::default(),
                 friend_modules: Default::default(),
                 enum_data: BTreeMap::new(),
@@ -3984,6 +3987,8 @@ pub struct ModuleData {
     /// Attributes attached to this module.
     attributes: Vec<Attribute>,
 
+    toplevel_attributes: expansion::ast::Attributes,
+
     /// Module byte code.
     pub module: CompiledModule,
 
@@ -4039,6 +4044,7 @@ impl ModuleData {
             source_map: SourceMap::new(MoveIrLoc::new(FileHash::empty(), 0, 0), ident),
             loc: Loc::default(),
             attributes: Default::default(),
+            toplevel_attributes: Default::default(),
             used_modules: Default::default(),
             friend_modules: Default::default(),
             enum_data: BTreeMap::new(),
@@ -4084,6 +4090,10 @@ impl<'env> ModuleEnv<'env> {
         &self.data.attributes
     }
 
+    pub fn get_toplevel_attributes(&self) -> &expansion::ast::Attributes {
+        &self.data.toplevel_attributes
+    }
+
     /// Returns full name as a string.
     pub fn get_full_name_str(&self) -> String {
         self.get_name().display_full(self.symbol_pool()).to_string()

crates/move-prover-boogie-backend/src/boogie_backend/bytecode_translator.rs

@@ -69,7 +69,7 @@ use crate::boogie_backend::{
         boogie_type_suffix_for_struct, boogie_well_formed_check, boogie_well_formed_expr_bv,
         FunctionTranslationStyle, TypeIdentToken,
     },
-    options::{BoogieFileMode, BoogieOptions},
+    options::BoogieOptions,
     spec_translator::SpecTranslator,
 };
 
@@ -379,9 +379,7 @@ impl<'env> BoogieTranslator<'env> {
                         }
                         // Attempt to emit Pure variant if eligible
                         // BUT: Don't emit Pure variants in spec_no_abort_check.bpl
-                        if !self.options.spec_no_abort_check_only
-                            && self.options.boogie_file_mode != BoogieFileMode::All
-                        {
+                        if !self.options.spec_no_abort_check_only {
                             self.translate_function_style(fun_env, FunctionTranslationStyle::Pure);
                         }
                     }
@@ -405,9 +403,7 @@ impl<'env> BoogieTranslator<'env> {
                         }
                         // Attempt to emit Pure variant if eligible
                         // BUT: Don't emit Pure variants in spec_no_abort_check.bpl
-                        if !self.options.spec_no_abort_check_only
-                            && self.options.boogie_file_mode != BoogieFileMode::All
-                        {
+                        if !self.options.spec_no_abort_check_only {
                             self.translate_function_style(fun_env, FunctionTranslationStyle::Pure);
                         }
                     }
@@ -493,18 +489,14 @@ impl<'env> BoogieTranslator<'env> {
         self.translate_function_style(fun_env, FunctionTranslationStyle::Aborts);
         self.translate_function_style(fun_env, FunctionTranslationStyle::Opaque);
 
-        if self.options.boogie_file_mode == BoogieFileMode::All
-            || self.targets.is_verified_spec(&fun_env.get_qualified_id())
-        {
+        if self.targets.is_verified_spec(&fun_env.get_qualified_id()) {
             self.translate_function_style(fun_env, FunctionTranslationStyle::Default);
             self.translate_function_style(fun_env, FunctionTranslationStyle::Asserts);
             self.translate_function_style(fun_env, FunctionTranslationStyle::SpecNoAbortCheck);
         }
         // Emit Pure variant if eligible (gated inside)
         // BUT: Don't emit Pure variants in spec_no_abort_check.bpl
-        if !self.options.spec_no_abort_check_only
-            && self.options.boogie_file_mode != BoogieFileMode::All
-        {
+        if !self.options.spec_no_abort_check_only {
             self.translate_function_style(fun_env, FunctionTranslationStyle::Pure);
         }
     }

crates/move-prover-boogie-backend/src/boogie_backend/options.rs

@@ -91,15 +91,13 @@ impl BorrowAggregate {
 pub enum BoogieFileMode {
     Function,
     Module,
-    All,
 }
 
 impl ToString for BoogieFileMode {
     fn to_string(&self) -> String {
         match self {
             BoogieFileMode::Function => "function".to_string(),
             BoogieFileMode::Module => "module".to_string(),
-            BoogieFileMode::All => "all".to_string(),
         }
     }
 }