From a299c144e1d1515feef51d20100159dfe258662e Mon Sep 17 00:00:00 2001
From: hegglinc <hegglinc@student.ethz.ch>
Date: Thu, 9 Mar 2023 19:30:20 +0100
Subject: [PATCH] Check if current package is primary package before throwing
 fake_error

In 2 places we throw fake errors to avoid caching of successes when we
should not. This lead to problems with local dependencies, since they are
verified too and the fake_error ended up being thrown too early. This
bug is resolved now.
---
 prusti/src/callbacks.rs | 32 ++++++++++++++++++++------------
 1 file changed, 20 insertions(+), 12 deletions(-)

diff --git a/prusti/src/callbacks.rs b/prusti/src/callbacks.rs
index 53873582a4f..ddb43206df5 100644
--- a/prusti/src/callbacks.rs
+++ b/prusti/src/callbacks.rs
@@ -148,20 +148,28 @@ impl prusti_rustc_interface::driver::Callbacks for PrustiCompilerCalls {
                 PrustiError::message(format!("compilerInfo{out}"), DUMMY_SP.into())
                     .emit(&env.diagnostic);
             }
+            // as long as we have to throw a fake error we need to check this
+            let is_primary_package = std::env::var("CARGO_PRIMARY_PACKAGE").is_ok();
 
             // collect and output Information used by IDE:
             if !config::no_verify() && !config::skip_verification() {
                 if let Some(target_def_path) = config::verify_only_defpath() {
-                    let procedures = annotated_procedures
-                        .into_iter()
-                        .filter(|x| env.name.get_unique_item_name(*x) == target_def_path)
-                        .collect();
-                    let selective_task = VerificationTask { procedures, types };
-                    // fake_error because otherwise a verification-success
-                    // (for a single method for example) will cause this result
-                    // to be cached by compiler at the moment
-                    verify(&env, def_spec, selective_task);
-                    fake_error(&env);
+                    // if we do selective verification, then definitely only
+                    // for methods of the primary package. Check needed because
+                    // of the fake_error, otherwise verification stops early
+                    // with local dependencies
+                    if is_primary_package {
+                        let procedures = annotated_procedures
+                            .into_iter()
+                            .filter(|x| env.name.get_unique_item_name(*x) == target_def_path)
+                            .collect();
+                        let selective_task = VerificationTask { procedures, types };
+                        // fake_error because otherwise a verification-success
+                        // (for a single method for example) will cause this result
+                        // to be cached by compiler at the moment
+                        verify(&env, def_spec, selective_task);
+                        fake_error(&env);
+                    }
                 } else {
                     let verification_task = VerificationTask {
                         procedures: annotated_procedures,
@@ -169,9 +177,9 @@ impl prusti_rustc_interface::driver::Callbacks for PrustiCompilerCalls {
                     };
                     verify(&env, def_spec, verification_task);
                 }
-            } else if config::skip_verification() && !config::no_verify() {
+            } else if config::skip_verification() && !config::no_verify() && is_primary_package {
                 // add a fake error, reason explained in issue #1261
-                fake_error(&env)
+                fake_error(&env);
             }
         });