Skip verification of prusti-contracts

.dockerignore

@@ -3,3 +3,4 @@ target/
 log/
 tmp/
 viper_tools/
+Dockerfile

Dockerfile

@@ -69,12 +69,12 @@ WORKDIR /root
 RUN cargo new good-example && \
     cd good-example && \
     sed -i '1s/^/use prusti_contracts::*;\n/;s/println.*$/assert!(true);/' src/main.rs && \
-    echo 'prusti-contracts = { path = "/opt/prusti-dev/prusti-contracts"}' >> Cargo.toml && \
+    echo 'prusti-contracts = { path = "/opt/prusti-dev/prusti-contracts" }' >> Cargo.toml && \
     cargo build && cargo clean && \
     cargo prusti && cargo clean
 RUN cargo new bad-example && \
     cd bad-example && \
     sed -i '1s/^/use prusti_contracts::*;\n/;s/println.*$/assert!(false);/' src/main.rs && \
-    echo 'prusti-contracts = { path = "/opt/prusti-dev/prusti-contracts"}' >> Cargo.toml && \
+    echo 'prusti-contracts = { path = "/opt/prusti-dev/prusti-contracts" }' >> Cargo.toml && \
     cargo build && cargo clean && \
     ! cargo prusti && cargo clean

prusti/Cargo.toml

@@ -13,7 +13,6 @@ doctest = false # and no doc tests
 [dependencies]
 env_logger = "0.8.2"
 prusti-contracts = { path = "../prusti-contracts", features = ["prusti"] }
-prusti-contracts-internal = { path = "../prusti-contracts-internal" }
 prusti-specs = { path = "../prusti-specs" }
 prusti-interface = { path = "../prusti-interface" }
 prusti-viper = { path = "../prusti-viper" }

prusti/src/driver.rs

@@ -119,17 +119,25 @@ fn init_loggers() {
     rustc_driver::init_rustc_env_logger();
 }
 
+const PRUSTI_PACKAGES: &'static [&'static str] = &[
+    "prusti_contracts_internal",
+    "prusti_contracts_impl",
+    "prusti_contracts",
+    "prusti_specs",
+];
+
 fn main() {
     // We assume that prusti-rustc already removed the first "rustc" argument
     // added by RUSTC_WRAPPER and all command line arguments -P<arg>=<val>
     // have been filtered out.
     let mut rustc_args = config::get_filtered_args();
 
-    // If the environment asks us to actually be rustc, or if lints have been disabled, then
-    // run `rustc` instead of Prusti.
+    // If the environment asks us to actually be rustc, or if lints have been disabled (which
+    // indicates that an upstream dependency is being compiled), then run `rustc` instead of Prusti.
     let prusti_be_rustc = config::be_rustc();
     let are_lints_disabled = arg_value(&rustc_args, "--cap-lints", |val| val == "allow").is_some();
-    if prusti_be_rustc || are_lints_disabled {
+    let is_prusti_package = env::var("CARGO_PKG_NAME").map(|name| PRUSTI_PACKAGES.contains(&name.as_str())).unwrap_or(false);
+    if prusti_be_rustc || are_lints_disabled || is_prusti_package {
         rustc_driver::main();
     }