Clippy in Regressions.

.github/workflows/format-check.yml

@@ -20,3 +20,20 @@ jobs:
         run: |
             pip3 install --upgrade autopep8
             ./scripts/run-autopep8.sh
+
+  clippy-check:
+    runs-on: ubuntu-20.04
+    steps:
+      - name: Checkout Kani
+        uses: actions/checkout@v2
+
+      - name: Setup Kani Dependencies
+        uses: ./.github/actions/setup
+        with:
+            os: ubuntu-20.04
+
+      - name: "Run Clippy"
+        run: |
+          cargo clippy --all -- -D warnings \
+          -A "clippy::expect_fun_call" \
+          -A "clippy::or_fun_call"

cprover_bindings/Cargo.toml

@@ -6,6 +6,7 @@ name = "cprover_bindings"
 version = "0.6.0"
 edition = "2021"
 license = "MIT OR Apache-2.0"
+publish = false
 
 [lib]
 test = true

cprover_bindings/src/lib.rs

@@ -29,6 +29,15 @@
 //! Speical [irep::Irep::id]s include:
 //! 1. [irep::IrepId::Empty] and [irep::IrepId::Nil] behaves like \[null\].
 
+// todo: Resolve the following clippy warnings.
+#![allow(
+    clippy::needless_bool,
+    clippy::let_and_return,
+    clippy::manual_map,
+    clippy::module_inception,
+    clippy::new_without_default
+)]
+
 mod env;
 pub mod goto_program;
 pub mod irep;

kani-compiler/Cargo.toml

@@ -6,6 +6,7 @@ name = "kani-compiler"
 version = "0.6.0"
 edition = "2021"
 license = "MIT OR Apache-2.0"
+publish = false
 
 [dependencies]
 ar = { version = "0.9.0", optional = true }

kani-compiler/kani_queries/Cargo.toml

@@ -6,6 +6,7 @@ name = "kani_queries"
 version = "0.6.0"
 edition = "2021"
 license = "MIT OR Apache-2.0"
+publish = false
 
 [dependencies]
 tracing = {version = "0.1"}

kani-compiler/src/main.rs

@@ -7,6 +7,26 @@
 //! Like miri, clippy, and other tools developed on the top of rustc, we rely on the
 //! rustc_private feature and a specific version of rustc.
 #![deny(warnings)]
+// todo: fix clippy warnings
+#![allow(
+    clippy::expect_fun_call,
+    clippy::explicit_auto_deref,
+    clippy::if_same_then_else,
+    clippy::iter_nth_zero,
+    clippy::let_and_return,
+    clippy::manual_map,
+    clippy::map_entry,
+    clippy::match_like_matches_macro,
+    clippy::module_inception,
+    clippy::needless_arbitrary_self_type,
+    clippy::needless_bool,
+    clippy::needless_return,
+    clippy::new_ret_no_self,
+    clippy::new_without_default,
+    clippy::or_fun_call,
+    clippy::redundant_clone,
+    clippy::type_complexity
+)]
 #![feature(extern_types)]
 #![recursion_limit = "256"]
 #![feature(box_patterns)]

kani-driver/Cargo.toml

@@ -9,6 +9,7 @@ description = "Build a project with Kani and run all proof harnesses"
 license = "MIT OR Apache-2.0"
 homepage = "https://github.com/model-checking/kani"
 repository = "https://github.com/model-checking/kani"
+publish = false
 
 [dependencies]
 kani_metadata = { path = "../kani_metadata" }

kani-driver/src/main.rs

@@ -1,6 +1,9 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
+// todo: resolve clippy warning.
+#![allow(clippy::unnecessary_lazy_evaluations)]
+
 use anyhow::Result;
 use args_toml::join_args;
 use call_cbmc::VerificationStatus;

kani_metadata/Cargo.toml

@@ -6,6 +6,7 @@ name = "kani_metadata"
 version = "0.6.0"
 edition = "2021"
 license = "MIT OR Apache-2.0"
+publish = false
 
 # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
 

library/kani/Cargo.toml

@@ -6,6 +6,7 @@ name = "kani"
 version = "0.6.0"
 edition = "2021"
 license = "MIT OR Apache-2.0"
+publish = false
 
 [dependencies]
 kani_macros = { path = "../kani_macros" }

library/kani/src/lib.rs

@@ -3,6 +3,9 @@
 #![feature(rustc_attrs)] // Used for rustc_diagnostic_item.
 #![feature(min_specialization)] // Used for default implementation of Arbitrary.
 
+// todo: resolve clippy warnings.
+#![allow(clippy::manual_range_contains, clippy::missing_safety_doc)]
+
 pub mod arbitrary;
 pub mod invariant;
 pub mod slice;

library/kani_macros/Cargo.toml

@@ -6,6 +6,7 @@ name = "kani_macros"
 version = "0.6.0"
 edition = "2021"
 license = "MIT OR Apache-2.0"
+publish = false
 
 [lib]
 proc-macro = true

library/kani_macros/src/lib.rs

@@ -8,6 +8,9 @@
 // So we have to enable this on the commandline (see kani-rustc) with:
 //   RUSTFLAGS="-Zcrate-attr=feature(register_tool) -Zcrate-attr=register_tool(kanitool)"
 
+// todo: resolve clippy warnings
+#![allow(clippy::len_zero, clippy::redundant_clone)]
+
 // proc_macro::quote is nightly-only, so we'll cobble things together instead
 use proc_macro::TokenStream;
 

library/std/Cargo.toml

@@ -8,6 +8,7 @@ name = "std"
 version = "0.6.0"
 edition = "2021"
 license = "MIT OR Apache-2.0"
+publish = false
 
 [dependencies]
 kani = {path="../kani"}

scripts/setup/macos-10.15/install_deps.sh

@@ -10,7 +10,7 @@ set -eux
 #brew update
 
 # Install dependencies via `brew`
-brew install universal-ctags wget
+brew install universal-ctags wget jq
 
 # Add Python package dependencies
 PYTHON_DEPS=(

scripts/setup/ubuntu/install_deps.sh

@@ -26,6 +26,7 @@ DEPS=(
   wget
   zlib1g
   zlib1g-dev
+  jq
 )
 
 # Version specific dependencies.

tools/bookrunner/Cargo.toml

@@ -6,6 +6,7 @@ name = "bookrunner"
 version = "0.1.0"
 edition = "2018"
 license = "MIT OR Apache-2.0"
+publish = false
 
 [dependencies]
 Inflector = "0.11.4"

tools/bookrunner/librustdoc/Cargo.toml

@@ -7,6 +7,8 @@ name = "rustdoc"
 version = "0.0.0"
 edition = "2021"
 license = "MIT OR Apache-2.0"
+publish = false
+
 # From upstream librustdoc:
 # https://github.com/rust-lang/rust/tree/master/src/librustdoc
 # Upstream crate does not list license but Rust statues:

tools/bookrunner/librustdoc/lib.rs

@@ -20,7 +20,12 @@
 #![feature(iter_intersperse)]
 #![recursion_limit = "256"]
 #![warn(rustc::internal)]
-#![allow(clippy::collapsible_if, clippy::collapsible_else_if)]
+#![allow(
+    clippy::collapsible_if,
+    clippy::collapsible_else_if,
+    clippy::derive_partial_eq_without_eq,
+    clippy::format_push_string
+)]
 
 #[macro_use]
 extern crate tracing;

tools/bookrunner/src/main.rs

@@ -2,6 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 #![feature(extend_one)]
 #![feature(rustc_private)]
+#![allow(clippy::too_many_arguments, clippy::redundant_clone, clippy::len_zero)]
 
 mod bookrunner;
 mod books;

tools/compiletest/Cargo.toml

@@ -8,6 +8,7 @@ name = "compiletest"
 version = "0.0.0"
 edition = "2021"
 license = "MIT OR Apache-2.0"
+publish = false
 # From upstream compiletest:
 # https://github.com/rust-lang/rust/tree/master/src/tools/compiletest
 # Upstream crate does not list license but Rust statues:

tools/compiletest/src/main.rs

@@ -3,6 +3,20 @@
 // Modifications Copyright Kani Contributors
 // See GitHub history for details.
 
+// todo: Resolve the following clippy warnings.
+#![allow(
+    clippy::collapsible_else_if,
+    clippy::derive_partial_eq_without_eq,
+    clippy::into_iter_on_ref,
+    clippy::iter_skip_next,
+    clippy::manual_strip,
+    clippy::needless_borrow,
+    clippy::needless_range_loop,
+    clippy::new_without_default,
+    clippy::ptr_arg,
+    clippy::single_char_pattern,
+    clippy::vec_init_then_push
+)]
 #![crate_name = "compiletest"]
 // The `test` crate is the only unstable feature
 // allowed here, just to share similar code.

tools/make-kani-release/Cargo.toml

@@ -7,6 +7,7 @@ version = "0.1.0"
 edition = "2021"
 description = "Contructs a Kani release bundle"
 license = "MIT OR Apache-2.0"
+publish = false
 
 [dependencies]
 anyhow = "1"