Revert model-checking#3080 except for std enablement

kani-compiler/src/args.rs

@@ -74,9 +74,6 @@ pub struct Arguments {
     /// Enable specific checks.
     #[clap(long)]
     pub ub_check: Vec<ExtraChecks>,
-    /// Ignore storage markers.
-    #[clap(long)]
-    pub ignore_storage_markers: bool,
 }
 
 #[derive(Debug, Clone, Copy, AsRefStr, EnumString, VariantNames, PartialEq, Eq)]

kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs

@@ -76,9 +76,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 self.codegen_set_discriminant(dest_ty, dest_expr, *variant_index, location)
             }
             StatementKind::StorageLive(var_id) => {
-                if self.queries.args().ignore_storage_markers
-                    || !self.current_fn().is_address_taken_local(*var_id)
-                {
+                if !self.current_fn().is_address_taken_local(*var_id) {
                     Stmt::skip(location)
                 } else {
                     let global_dead_object = self.ensure_global_var(
@@ -102,9 +100,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 }
             }
             StatementKind::StorageDead(var_id) => {
-                if self.queries.args().ignore_storage_markers
-                    || !self.current_fn().is_address_taken_local(*var_id)
-                {
+                if !self.current_fn().is_address_taken_local(*var_id) {
                     Stmt::skip(location)
                 } else {
                     let global_dead_object = self.ensure_global_var(

kani-driver/src/args/mod.rs

@@ -252,14 +252,6 @@ pub struct VerificationArgs {
     #[arg(long, hide_short_help = true, requires("enable_unstable"))]
     pub ignore_global_asm: bool,
 
-    /// Ignore lifetimes of local variables. This effectively extends their
-    /// lifetimes to the function scope, and hence may cause Kani to miss
-    /// undefined behavior resulting from using the variable after it dies.
-    /// This option may impact the soundness of the analysis and may cause false
-    /// proofs and/or counterexamples
-    #[arg(long, hide_short_help = true, requires("enable_unstable"))]
-    pub ignore_locals_lifetime: bool,
-
     /// Write the GotoC symbol table to a file in JSON format instead of goto binary format.
     #[arg(long, hide_short_help = true)]
     pub write_json_symtab: bool,

kani-driver/src/call_single_file.rs

@@ -105,10 +105,6 @@ impl KaniSession {
             flags.push("--ub-check=validity".into())
         }
 
-        if self.args.ignore_locals_lifetime {
-            flags.push("--ignore-storage-markers".into())
-        }
-
         flags.extend(self.args.common_args.unstable_features.as_arguments().map(str::to_string));
 
         // This argument will select the Kani flavour of the compiler. It will be removed before

tests/perf/btreeset/insert_any/Cargo.toml

@@ -9,8 +9,3 @@ edition = "2021"
 # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
 
 [dependencies]
-
-# Temporarily ignore the handling of storage markers till
-# https://github.com/model-checking/kani/issues/3099 is fixed
-[package.metadata.kani]
-flags = { ignore-locals-lifetime = true, enable-unstable = true }

tests/perf/btreeset/insert_multi/Cargo.toml

@@ -9,8 +9,3 @@ edition = "2021"
 # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
 
 [dependencies]
-
-# Temporarily ignore the handling of storage markers till
-# https://github.com/model-checking/kani/issues/3099 is fixed
-[package.metadata.kani]
-flags = { ignore-locals-lifetime = true, enable-unstable = true }

tests/perf/btreeset/insert_same/Cargo.toml

@@ -9,8 +9,3 @@ edition = "2021"
 # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
 
 [dependencies]
-
-# Temporarily ignore the handling of storage markers till
-# https://github.com/model-checking/kani/issues/3099 is fixed
-[package.metadata.kani]
-flags = { ignore-locals-lifetime = true, enable-unstable = true }

tests/perf/hashset/Cargo.toml

@@ -12,8 +12,3 @@ description = "Verify HashSet basic behavior"
 
 [package.metadata.kani.unstable]
 stubbing = true
-
-# Temporarily ignore the handling of storage markers till
-# https://github.com/model-checking/kani/issues/3099 is fixed
-[package.metadata.kani]
-flags = { ignore-locals-lifetime = true, enable-unstable = true }