Adds functionality to ignore dependencies contracts

prusti-utils/src/config.rs

@@ -130,6 +130,7 @@ lazy_static::lazy_static! {
         settings.set_default::<Option<u8>>("number_of_parallel_verifiers", None).unwrap();
         settings.set_default::<Option<String>>("min_prusti_version", None).unwrap();
         settings.set_default("num_errors_per_function", 1).unwrap();
+        settings.set_default("ignore_deps_contracts", false).unwrap();
 
         settings.set_default("print_desugared_specs", false).unwrap();
         settings.set_default("print_typeckd_specs", false).unwrap();
@@ -1030,3 +1031,8 @@ pub fn enable_type_invariants() -> bool {
 pub fn num_errors_per_function() -> u32 {
     read_setting("num_errors_per_function")
 }
+
+/// When enabled Prusti won't collect contracts from the project's dependencies
+pub fn ignore_deps_contracts() -> bool {
+    read_setting("ignore_deps_contracts")
+}

prusti/src/driver.rs

@@ -89,16 +89,18 @@ fn main() {
         val == "build_script_build"
     })
     .is_some();
-    if config::be_rustc() || build_script_build {
+
+    // This environment variable will not be set when building dependencies.
+    let is_primary_package = env::var("CARGO_PRIMARY_PACKAGE").is_ok();
+
+    if config::be_rustc() || build_script_build || (!is_primary_package && config::ignore_deps_contracts()) {
         driver::main();
     }
 
     // Initialize Prusti and the Rust compiler loggers.
     // This must be done after the build script check, otherwise Tokio's global tracing will fail.
     let _log_flush_guard = init_loggers();
 
-    // This environment variable will not be set when building dependencies.
-    let is_primary_package = env::var("CARGO_PRIMARY_PACKAGE").is_ok();
     // Is this crate a dependency when user doesn't want to verify dependencies
     let is_no_verify_dep_crate = !is_primary_package && config::no_verify_deps();