Address PR comments

Author: celinval

docs/src/rustc-hacks.md

@@ -52,27 +52,19 @@ Note that pretty printing for the Rust nightly toolchain (which Kani uses) is no
 For example, a vector may be displayed as `vec![{...}, {...}]` on nightly Rust, when it would be displayed as `vec![Some(0), None]` on stable Rust.
 Hopefully, this will be fixed soon.
 
-### RustRover / CLion
+### CLion / IntelliJ
 This is not a great solution, but it works for now (see <https://github.com/intellij-rust/intellij-rust/issues/1618>
 for more details).
-
-Open the `Cargo.toml` of your crate (e.g.: `kani-compiler`), and do the following:
-
-1. Add optional dependencies on the `rustc` crates you are using.
-2. Add a feature that enable those dependencies.
-3. Toggle that feature using the IDE GUI.
-
-Here is an example:
+Edit the `Cargo.toml` of the package that you're working on and add artificial dependencies on the `rustc` packages that you would like to explore.
 
 ```toml
-# ** At the bottom of the dependencies section: **
+# This configuration doesn't exist so it shouldn't affect your build.
+[target.'cfg(KANI_DEV)'.dependencies]
 # Adjust the path here to point to a local copy of the rust compiler.
-# E.g.: ~/.rustup/toolchains/<toolchain>/lib/rustlib/rustc-src/rust/compiler
-rustc_smir = { path = "<path_to_rustc>/rustc_smir", optional = true }
-stable_mir = { path = "<path_to_rustc>/stable_mir", optional = true }
-
-[features]
-clion = ['rustc_smir', 'stable_mir']
+# The best way is to use the rustup path. Replace <toolchain> with the
+# proper name to your toolchain.
+rustc_driver = { path = "~/.rustup/toolchains/<toolchain>/lib/rustlib/rustc-src/rust/compiler/rustc_driver" }
+rustc_interface = { path = "~/.rustup/toolchains/<toolchain>/lib/rustlib/rustc-src/rust/compiler/rustc_interface" }
 ```
 
 **Don't forget to rollback the changes before you create your PR.**

tests/script-based-pre/tool-scanner/scanner-test.expected

@@ -1,6 +1,7 @@
 5 test_scan_fn_loops.csv
 20 test_scan_functions.csv
 5 test_scan_input_tys.csv
-16 test_scan_overall.csv
+17 test_scan_overall.csv
 3 test_scan_recursion.csv
+9 test_scan_unsafe_distance.csv
 6 test_scan_unsafe_ops.csv

tests/script-based-pre/tool-scanner/test.rs

@@ -14,11 +14,6 @@ pub fn generic<T: Default>() -> T {
     T::default()
 }
 
-pub fn blah() {
-    ok();
-    assert_eq!(u8::default(), 0);
-}
-
 pub struct RecursiveType {
     pub inner: Option<*const RecursiveType>,
 }
@@ -112,6 +107,7 @@ extern "C" {
     fn external_function();
 }
 
+/// Ensure scanner finds unsafe calls to external functions.
 pub fn call_external() {
     unsafe { external_function() };
 }

tools/scanner/src/analysis.rs

@@ -1,7 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-//! Provide different static analysis to be performed in the crate under compilation
+//! Provide passes that perform intra-function analysis on the crate under compilation
 
 use crate::info;
 use csv::WriterBuilder;
@@ -253,11 +253,11 @@ macro_rules! fn_props {
         }
 
         impl $name {
-            pub const fn num_props() -> usize {
+            $vis const fn num_props() -> usize {
                 [$(stringify!($prop),)+].len()
             }
 
-            pub fn new(fn_name: String) -> Self {
+            $vis fn new(fn_name: String) -> Self {
                 Self { fn_name, $($prop: 0,)+}
             }
         }

tools/scanner/src/call_graph.rs

@@ -1,7 +1,11 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-//! Provide different static analysis to be performed in the call graph
+//! Provide passes that perform inter-function analysis on the crate under compilation.
+//!
+//! This module also includes a `CallGraph` structure to help the analysis.
+//! For now, we build the CallGraph as part of the pass, but as we add more analysis,
+//! the call-graph could be reused by different analysis.
 
 use crate::analysis::{FnCallVisitor, FnUnsafeOperations, OverallStats};
 use stable_mir::mir::{MirVisitor, Safety};