Merge pull request #1496 from nshyrei/ignore_deps_contracts

Adds functionality to ignore dependencies contracts

docs/dev-guide/src/config/flags.md

@@ -47,6 +47,7 @@
 | [`MIN_PRUSTI_VERSION`](#min_prusti_version) | `Option<String>` | `None` | A |
 | [`NO_VERIFY`](#no_verify) | `bool` | `false` | A |
 | [`NO_VERIFY_DEPS`](#no_verify_deps) | `bool` | `false` | B |
+| [`IGNORE_DEPS_CONTRACTS`](#ignore_deps_contracts) | `bool` | `false` | B |
 | [`OPT_IN_VERIFICATION`](#opt_in_verification) | `bool` | `false` | A |
 | [`OPTIMIZATIONS`](#optimizations) | `Vec<String>` | "all" | A |
 | [`PRESERVE_SMT_TRACE_FILES`](#preserve_smt_trace_files) | `bool` | `false` | A |
@@ -302,7 +303,12 @@ When enabled, verification is skipped for dependencies. Equivalent to enabling `
 
 > **Note:** applied to all dependency crates when running with `cargo prusti`.
 
+## `IGNORE_DEPS_CONTRACTS`
+
+When enabled, Prusti will not collect contracts from the project's dependencies. This is useful for debugging and working around unsupported language features in the dependencies.
+
 ## `OPT_IN_VERIFICATION`
+
 When enabled, Prusti will only try to verify the functions annotated with `#[verified]`. All other functions are assumed to be `#[trusted]`, by default. Functions annotated with both `#[trusted]` and `#[verified]` will not be verified.
 
 ## `ONLY_MEMORY_SAFETY`

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,21 @@ 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();