From 6777e7c8e7230802f39fa223e6fd383d51ecb286 Mon Sep 17 00:00:00 2001 From: Jaisurya Nanduri Date: Tue, 20 Aug 2024 19:37:30 +0000 Subject: [PATCH 01/10] Upgrade toolchain to 08/20 --- .../src/codegen_cprover_gotoc/codegen/typ.rs | 7 +- kani-compiler/src/kani_middle/coercion.rs | 2 +- .../points_to/points_to_analysis.rs | 4 +- .../src/kani_middle/transform/internal_mir.rs | 7 +- kani-compiler/src/session.rs | 3 +- rust-toolchain.toml | 2 +- .../tool-scanner/output_dir/test.rs | 77 +++++++++++++++++++ tools/scanner/Cargo.toml | 1 - 8 files changed, 91 insertions(+), 12 deletions(-) create mode 100644 tests/script-based-pre/tool-scanner/output_dir/test.rs diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index 9baa3c59f4c2..016bf0d3a261 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs @@ -579,7 +579,10 @@ impl<'tcx> GotocCtx<'tcx> { .unwrap(); self.codegen_fndef_type(instance) } - ty::FnPtr(sig) => self.codegen_function_sig(*sig).to_pointer(), + ty::FnPtr(sig_tys, hdr) => { + let sig = sig_tys.with(*hdr); + self.codegen_function_sig(sig).to_pointer() + } ty::Closure(_, subst) => self.codegen_ty_closure(ty, subst), ty::Coroutine(..) => self.codegen_ty_coroutine(ty), ty::Never => self.ensure_struct(NEVER_TYPE_EMPTY_STRUCT_NAME, "!", |_, _| vec![]), @@ -1014,7 +1017,7 @@ impl<'tcx> GotocCtx<'tcx> { // These types were blocking stdlib. Doing the default thing to unblock. // https://github.com/model-checking/kani/issues/214 - ty::FnPtr(_) => self.codegen_ty(pointee_type).to_pointer(), + ty::FnPtr(_, _) => self.codegen_ty(pointee_type).to_pointer(), // These types have no regression tests for them. // For soundness, hold off on generating them till we have test-cases. diff --git a/kani-compiler/src/kani_middle/coercion.rs b/kani-compiler/src/kani_middle/coercion.rs index 822f32631e0c..38760fca300d 100644 --- a/kani-compiler/src/kani_middle/coercion.rs +++ b/kani-compiler/src/kani_middle/coercion.rs @@ -99,7 +99,7 @@ pub fn extract_unsize_casting<'tcx>( coerce_info.dst_ty )); // Find the tail of the coercion that determines the type of metadata to be stored. - let (src_base_ty, dst_base_ty) = tcx.struct_lockstep_tails_erasing_lifetimes( + let (src_base_ty, dst_base_ty) = tcx.struct_lockstep_tails_for_codegen( src_pointee_ty, dst_pointee_ty, ParamEnv::reveal_all(), diff --git a/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs b/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs index eff7dd1fc486..68343ccaad37 100644 --- a/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs +++ b/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs @@ -53,7 +53,7 @@ struct PointsToAnalysis<'a, 'tcx> { tcx: TyCtxt<'tcx>, /// This will be used in the future to resolve function pointer and vtable calls. Currently, we /// can resolve call graph edges just by looking at the terminators and erroring if we can't - /// resolve the callee. + /// resolve the callee. call_graph: &'a CallGraph, /// This graph should contain a subset of the points-to graph reachable from function arguments. /// For the entry function it will be empty (as it supposedly does not have any parameters). @@ -521,7 +521,7 @@ impl<'a, 'tcx> PointsToAnalysis<'a, 'tcx> { | Rvalue::ShallowInitBox(operand, _) | Rvalue::Cast(_, operand, _) | Rvalue::Repeat(operand, ..) => self.successors_for_operand(state, operand), - Rvalue::Ref(_, _, ref_place) | Rvalue::AddressOf(_, ref_place) => { + Rvalue::Ref(_, _, ref_place) | Rvalue::RawPtr(_, ref_place) => { // Here, a reference to a place is created, which leaves the place // unchanged. state.resolve_place(ref_place, self.instance) diff --git a/kani-compiler/src/kani_middle/transform/internal_mir.rs b/kani-compiler/src/kani_middle/transform/internal_mir.rs index 0dcf7d47c13a..ba23fbf2dddf 100644 --- a/kani-compiler/src/kani_middle/transform/internal_mir.rs +++ b/kani-compiler/src/kani_middle/transform/internal_mir.rs @@ -210,10 +210,9 @@ impl RustcInternalMir for Rvalue { fn internal_mir<'tcx>(&self, tcx: TyCtxt<'tcx>) -> Self::T<'tcx> { match self { - Rvalue::AddressOf(mutability, place) => rustc_middle::mir::Rvalue::AddressOf( - internal(tcx, mutability), - internal(tcx, place), - ), + Rvalue::AddressOf(mutability, place) => { + rustc_middle::mir::Rvalue::RawPtr(internal(tcx, mutability), internal(tcx, place)) + } Rvalue::Aggregate(aggregate_kind, operands) => rustc_middle::mir::Rvalue::Aggregate( Box::new(aggregate_kind.internal_mir(tcx)), rustc_index::IndexVec::from_raw( diff --git a/kani-compiler/src/session.rs b/kani-compiler/src/session.rs index 7ec2b79a0469..ed902c1c138a 100644 --- a/kani-compiler/src/session.rs +++ b/kani-compiler/src/session.rs @@ -60,7 +60,8 @@ static JSON_PANIC_HOOK: LazyLock) + Sync + Lrc::new(SourceMap::new(FilePathMapping::empty())), fallback_bundle, false, - HumanReadableErrorType::Default(ColorConfig::Never), + HumanReadableErrorType::Default, + ColorConfig::Never, ); let diagnostic = DiagInner::new(rustc_errors::Level::Bug, msg); emitter.emit_diagnostic(diagnostic); diff --git a/rust-toolchain.toml b/rust-toolchain.toml index e3b6229d73c6..4cfd7bad9312 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -2,5 +2,5 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [toolchain] -channel = "nightly-2024-08-07" +channel = "nightly-2024-08-20" components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"] diff --git a/tests/script-based-pre/tool-scanner/output_dir/test.rs b/tests/script-based-pre/tool-scanner/output_dir/test.rs new file mode 100644 index 000000000000..24b346e535b5 --- /dev/null +++ b/tests/script-based-pre/tool-scanner/output_dir/test.rs @@ -0,0 +1,77 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +//! Sanity check for the utility tool `scanner`. + +pub fn check_outer_coercion() { + assert!(false); +} + +unsafe fn do_nothing() {} + +pub fn generic() -> T { + unsafe { do_nothing() }; + T::default() +} + +pub struct RecursiveType { + pub inner: Option<*const RecursiveType>, +} + +pub enum RecursiveEnum { + Base, + Recursion(Box), + RefCell(std::cell::RefCell), +} + +pub fn recursive_type(input1: RecursiveType, input2: RecursiveEnum) { + let _ = (input1, input2); +} + +pub fn with_iterator(input: &[usize]) -> usize { + input + .iter() + .copied() + .find(|e| *e == 0) + .unwrap_or_else(|| input.iter().fold(0, |acc, i| acc + 1)) +} + +static mut COUNTER: Option = Some(0); +static OK: bool = true; + +pub unsafe fn next_id() -> usize { + let sum = COUNTER.unwrap() + 1; + COUNTER = Some(sum); + sum +} + +pub unsafe fn current_id() -> usize { + COUNTER.unwrap() +} + +pub fn ok() -> bool { + OK +} + +pub unsafe fn raw_to_ref<'a, T>(raw: *const T) -> &'a T { + &*raw +} + +pub fn recursion_begin(stop: bool) { + if !stop { + recursion_tail() + } +} + +pub fn recursion_tail() { + recursion_begin(false); + not_recursive(); +} + +pub fn start_recursion() { + recursion_begin(true); +} + +pub fn not_recursive() { + let _ = ok(); +} diff --git a/tools/scanner/Cargo.toml b/tools/scanner/Cargo.toml index edbd330bea47..2eb8ec07e098 100644 --- a/tools/scanner/Cargo.toml +++ b/tools/scanner/Cargo.toml @@ -20,4 +20,3 @@ strum_macros = "0.26" # This crate uses rustc crates. # More info: https://github.com/rust-analyzer/rust-analyzer/pull/7891 rustc_private = true - From 9bf5f8da82656e773b1ff7aac64d88cc10d68539 Mon Sep 17 00:00:00 2001 From: Jaisurya Nanduri Date: Tue, 20 Aug 2024 19:39:41 +0000 Subject: [PATCH 02/10] Remove leftover test file --- .../tool-scanner/output_dir/test.rs | 77 ------------------- 1 file changed, 77 deletions(-) delete mode 100644 tests/script-based-pre/tool-scanner/output_dir/test.rs diff --git a/tests/script-based-pre/tool-scanner/output_dir/test.rs b/tests/script-based-pre/tool-scanner/output_dir/test.rs deleted file mode 100644 index 24b346e535b5..000000000000 --- a/tests/script-based-pre/tool-scanner/output_dir/test.rs +++ /dev/null @@ -1,77 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT -// -//! Sanity check for the utility tool `scanner`. - -pub fn check_outer_coercion() { - assert!(false); -} - -unsafe fn do_nothing() {} - -pub fn generic() -> T { - unsafe { do_nothing() }; - T::default() -} - -pub struct RecursiveType { - pub inner: Option<*const RecursiveType>, -} - -pub enum RecursiveEnum { - Base, - Recursion(Box), - RefCell(std::cell::RefCell), -} - -pub fn recursive_type(input1: RecursiveType, input2: RecursiveEnum) { - let _ = (input1, input2); -} - -pub fn with_iterator(input: &[usize]) -> usize { - input - .iter() - .copied() - .find(|e| *e == 0) - .unwrap_or_else(|| input.iter().fold(0, |acc, i| acc + 1)) -} - -static mut COUNTER: Option = Some(0); -static OK: bool = true; - -pub unsafe fn next_id() -> usize { - let sum = COUNTER.unwrap() + 1; - COUNTER = Some(sum); - sum -} - -pub unsafe fn current_id() -> usize { - COUNTER.unwrap() -} - -pub fn ok() -> bool { - OK -} - -pub unsafe fn raw_to_ref<'a, T>(raw: *const T) -> &'a T { - &*raw -} - -pub fn recursion_begin(stop: bool) { - if !stop { - recursion_tail() - } -} - -pub fn recursion_tail() { - recursion_begin(false); - not_recursive(); -} - -pub fn start_recursion() { - recursion_begin(true); -} - -pub fn not_recursive() { - let _ = ok(); -} From 4556921d73aa571508145240cfd0ceefde30efce Mon Sep 17 00:00:00 2001 From: Jaisurya Nanduri Date: Mon, 26 Aug 2024 16:43:52 +0000 Subject: [PATCH 03/10] Update to 08/26 --- rust-toolchain.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 4cfd7bad9312..af6c82c0377d 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -2,5 +2,5 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [toolchain] -channel = "nightly-2024-08-20" +channel = "nightly-2024-08-26" components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"] From c8bfdb06412774b78cfe0ac2d5c178463965c463 Mon Sep 17 00:00:00 2001 From: Jaisurya Nanduri Date: Tue, 27 Aug 2024 20:18:47 +0000 Subject: [PATCH 04/10] Upgrade to 8/27 and fix breaks in cargo --- kani-driver/src/call_cargo.rs | 8 +++++++- rust-toolchain.toml | 2 +- tools/scanner/src/bin/scan.rs | 1 + 3 files changed, 9 insertions(+), 2 deletions(-) diff --git a/kani-driver/src/call_cargo.rs b/kani-driver/src/call_cargo.rs index 4e8e83b562af..99a145cecfd1 100644 --- a/kani-driver/src/call_cargo.rs +++ b/kani-driver/src/call_cargo.rs @@ -73,6 +73,11 @@ impl KaniSession { cargo_args.push("-v".into()); } + // We need this suffix push because of https://github.com/rust-lang/cargo/pull/14370 + // which removes the library suffix from the build-std command + let mut full_path = std_path.to_path_buf(); + full_path.push("library"); + // Since we are verifying the standard library, we set the reachability to all crates. let mut cmd = setup_cargo_command()?; cmd.args(&cargo_args) @@ -82,7 +87,7 @@ impl KaniSession { // https://doc.rust-lang.org/cargo/reference/environment-variables.html .env("CARGO_ENCODED_RUSTFLAGS", rustc_args.join(OsStr::new("\x1f"))) .env("CARGO_TERM_PROGRESS_WHEN", "never") - .env("__CARGO_TESTS_ONLY_SRC_ROOT", std_path.as_os_str()); + .env("__CARGO_TESTS_ONLY_SRC_ROOT", full_path.as_os_str()); Ok(self .run_build(cmd)? @@ -239,6 +244,7 @@ impl KaniSession { fn run_build(&self, cargo_cmd: Command) -> Result> { let support_color = std::io::stdout().is_terminal(); let mut artifacts = vec![]; + println!("The cargo cmd is {:?}", cargo_cmd); if let Some(mut cargo_process) = self.run_piped(cargo_cmd)? { let reader = BufReader::new(cargo_process.stdout.take().unwrap()); let mut error_count = 0; diff --git a/rust-toolchain.toml b/rust-toolchain.toml index af6c82c0377d..9e7bd732ce8f 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -2,5 +2,5 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [toolchain] -channel = "nightly-2024-08-26" +channel = "nightly-2024-08-27" components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"] diff --git a/tools/scanner/src/bin/scan.rs b/tools/scanner/src/bin/scan.rs index 92b5319ec780..197b34d23422 100644 --- a/tools/scanner/src/bin/scan.rs +++ b/tools/scanner/src/bin/scan.rs @@ -14,6 +14,7 @@ //! together with the name of the analysis. //! //! Look at each analysis documentation to see which files an analysis produces. +#![feature(rustc_private)] use scanner::run_all; use std::process::ExitCode; From 825e88033f8c9537d1ec11c3c9e72a2c89f2b891 Mon Sep 17 00:00:00 2001 From: Jaisurya Nanduri Date: Wed, 28 Aug 2024 12:16:55 +0000 Subject: [PATCH 05/10] Update to 08/28 --- rust-toolchain.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 9e7bd732ce8f..3421b9b3adc9 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -2,5 +2,5 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [toolchain] -channel = "nightly-2024-08-27" +channel = "nightly-2024-08-28" components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"] From 6e07c0594ad8d899682bcff4bde3e4fd3df1c4cd Mon Sep 17 00:00:00 2001 From: Jaisurya Nanduri Date: Wed, 28 Aug 2024 12:19:33 +0000 Subject: [PATCH 06/10] Fix clippy errors --- kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs | 1 + 1 file changed, 1 insertion(+) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs index d0e3fc3f442f..fba1a4c3ced5 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs @@ -832,6 +832,7 @@ fn projection_data_ptr(projection: &ProjectedPlace) -> Expr { /// Err` if it is `Ok` and returns an `codegen_unimplemented` /// expression otherwise. /// Note that this macro affects the control flow since it calls `return` +#[allow(clippy::too_long_first_doc_paragraph)] #[macro_export] macro_rules! unwrap_or_return_codegen_unimplemented { ($ctx:expr, $pp_result:expr) => {{ From d35186e1016083c6cc9e2b93c56600480c258ac5 Mon Sep 17 00:00:00 2001 From: Jaisurya Nanduri Date: Wed, 28 Aug 2024 12:31:05 +0000 Subject: [PATCH 07/10] Remove unnecessary print statements --- kani-driver/src/call_cargo.rs | 1 - 1 file changed, 1 deletion(-) diff --git a/kani-driver/src/call_cargo.rs b/kani-driver/src/call_cargo.rs index 36043f4494df..ef289cead4c2 100644 --- a/kani-driver/src/call_cargo.rs +++ b/kani-driver/src/call_cargo.rs @@ -244,7 +244,6 @@ impl KaniSession { fn run_build(&self, cargo_cmd: Command) -> Result> { let support_color = std::io::stdout().is_terminal(); let mut artifacts = vec![]; - println!("The cargo cmd is {:?}", cargo_cmd); if let Some(mut cargo_process) = self.run_piped(cargo_cmd)? { let reader = BufReader::new(cargo_process.stdout.take().unwrap()); let mut error_count = 0; From df4008ece70f3fc4ac995b73229c22cba97628d8 Mon Sep 17 00:00:00 2001 From: Jaisurya Nanduri Date: Wed, 28 Aug 2024 16:33:11 +0000 Subject: [PATCH 08/10] Add a blanket allow across the workspace for "too_long_first_doc_paragraph" --- Cargo.toml | 3 +++ cprover_bindings/Cargo.toml | 3 +++ kani-compiler/Cargo.toml | 3 +++ kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs | 1 - kani_metadata/Cargo.toml | 3 +++ library/kani/Cargo.toml | 3 +++ library/kani_core/Cargo.toml | 3 +++ library/kani_macros/Cargo.toml | 3 +++ library/kani_macros/src/lib.rs | 2 +- tools/compiletest/Cargo.toml | 3 +++ 10 files changed, 25 insertions(+), 2 deletions(-) diff --git a/Cargo.toml b/Cargo.toml index f2301983fcb4..149b8d2c93c8 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -71,3 +71,6 @@ exclude = [ "tests/script-based-pre/build-cache-dirty/target/new_dep", "tests/script-based-pre/verify_std_cmd/tmp_dir/target/kani_verify_std", ] + +[workspace.lints.clippy] +too_long_first_doc_paragraph = "allow" diff --git a/cprover_bindings/Cargo.toml b/cprover_bindings/Cargo.toml index c53ffb207fcf..b0e3c578bbcf 100644 --- a/cprover_bindings/Cargo.toml +++ b/cprover_bindings/Cargo.toml @@ -24,3 +24,6 @@ linear-map = {version = "1.2", features = ["serde_impl"]} [dev-dependencies] serde_test = "1" memuse = "0.2.1" + +[lints] +workspace = true diff --git a/kani-compiler/Cargo.toml b/kani-compiler/Cargo.toml index fcb33b8074e4..fc06c393f3eb 100644 --- a/kani-compiler/Cargo.toml +++ b/kani-compiler/Cargo.toml @@ -35,3 +35,6 @@ write_json_symtab = [] [package.metadata.rust-analyzer] # This package uses rustc crates. rustc_private=true + +[lints] +workspace = true diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs index fba1a4c3ced5..d0e3fc3f442f 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs @@ -832,7 +832,6 @@ fn projection_data_ptr(projection: &ProjectedPlace) -> Expr { /// Err` if it is `Ok` and returns an `codegen_unimplemented` /// expression otherwise. /// Note that this macro affects the control flow since it calls `return` -#[allow(clippy::too_long_first_doc_paragraph)] #[macro_export] macro_rules! unwrap_or_return_codegen_unimplemented { ($ctx:expr, $pp_result:expr) => {{ diff --git a/kani_metadata/Cargo.toml b/kani_metadata/Cargo.toml index de91900d6d9c..efa28288d148 100644 --- a/kani_metadata/Cargo.toml +++ b/kani_metadata/Cargo.toml @@ -16,3 +16,6 @@ cbmc = { path = "../cprover_bindings", package = "cprover_bindings" } strum = "0.26" strum_macros = "0.26" clap = { version = "4.4.11", features = ["derive"] } + +[lints] +workspace = true diff --git a/library/kani/Cargo.toml b/library/kani/Cargo.toml index 7d7ced8ee0b7..a3692f95e3f5 100644 --- a/library/kani/Cargo.toml +++ b/library/kani/Cargo.toml @@ -15,3 +15,6 @@ kani_core = { path = "../kani_core" } [features] concrete_playback = [] no_core=["kani_macros/no_core"] + +[lints] +workspace = true diff --git a/library/kani_core/Cargo.toml b/library/kani_core/Cargo.toml index 8928992c3f16..9df828e77c5a 100644 --- a/library/kani_core/Cargo.toml +++ b/library/kani_core/Cargo.toml @@ -14,3 +14,6 @@ kani_macros = { path = "../kani_macros"} [features] no_core=["kani_macros/no_core"] + +[lints] +workspace = true diff --git a/library/kani_macros/Cargo.toml b/library/kani_macros/Cargo.toml index 475e2978df91..574960e5fc0a 100644 --- a/library/kani_macros/Cargo.toml +++ b/library/kani_macros/Cargo.toml @@ -23,3 +23,6 @@ rustc_private = true [features] no_core = [] + +[lints] +workspace = true diff --git a/library/kani_macros/src/lib.rs b/library/kani_macros/src/lib.rs index 6fe0979f08bc..63ed990a4840 100644 --- a/library/kani_macros/src/lib.rs +++ b/library/kani_macros/src/lib.rs @@ -8,7 +8,6 @@ // So we have to enable this on the commandline (see kani-rustc) with: // RUSTFLAGS="-Zcrate-attr=feature(register_tool) -Zcrate-attr=register_tool(kanitool)" #![feature(proc_macro_diagnostic)] - mod derive; // proc_macro::quote is nightly-only, so we'll cobble things together instead @@ -65,6 +64,7 @@ pub fn recursion(attr: TokenStream, item: TokenStream) -> TokenStream { /// Set Loop unwind limit for proof harnesses /// The attribute `#[kani::unwind(arg)]` can only be called alongside `#[kani::proof]`. /// arg - Takes in a integer value (u32) that represents the unwind value for the harness. +#[allow(clippy::too_long_first_doc_paragraph)] #[proc_macro_attribute] pub fn unwind(attr: TokenStream, item: TokenStream) -> TokenStream { attr_impl::unwind(attr, item) diff --git a/tools/compiletest/Cargo.toml b/tools/compiletest/Cargo.toml index 78a90d9aae38..967bc1715525 100644 --- a/tools/compiletest/Cargo.toml +++ b/tools/compiletest/Cargo.toml @@ -30,3 +30,6 @@ wait-timeout = "0.2.0" [target.'cfg(unix)'.dependencies] libc = "0.2" + +[lints] +workspace = true From beb375d187d78dec0bbf6e9b77e7cc5da90150e4 Mon Sep 17 00:00:00 2001 From: Jaisurya Nanduri Date: Wed, 28 Aug 2024 16:36:48 +0000 Subject: [PATCH 09/10] Revert whitespace change --- kani-compiler/src/kani_middle/points_to/points_to_analysis.rs | 2 +- tools/scanner/Cargo.toml | 1 + 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs b/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs index 68343ccaad37..9cd2a63a2d98 100644 --- a/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs +++ b/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs @@ -53,7 +53,7 @@ struct PointsToAnalysis<'a, 'tcx> { tcx: TyCtxt<'tcx>, /// This will be used in the future to resolve function pointer and vtable calls. Currently, we /// can resolve call graph edges just by looking at the terminators and erroring if we can't - /// resolve the callee. + /// resolve the callee. call_graph: &'a CallGraph, /// This graph should contain a subset of the points-to graph reachable from function arguments. /// For the entry function it will be empty (as it supposedly does not have any parameters). diff --git a/tools/scanner/Cargo.toml b/tools/scanner/Cargo.toml index ce006fa4eabe..f27e9e06c72c 100644 --- a/tools/scanner/Cargo.toml +++ b/tools/scanner/Cargo.toml @@ -22,3 +22,4 @@ graph-cycles = "0.1.0" # This crate uses rustc crates. # More info: https://github.com/rust-analyzer/rust-analyzer/pull/7891 rustc_private = true + From cd53bcf04f94d7fc0cde228fa5dc5ca75a82bfa6 Mon Sep 17 00:00:00 2001 From: Jaisurya Nanduri Date: Wed, 28 Aug 2024 16:37:18 +0000 Subject: [PATCH 10/10] Cargo fmt + clippy --- kani-compiler/src/kani_middle/points_to/points_to_analysis.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs b/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs index 9cd2a63a2d98..68343ccaad37 100644 --- a/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs +++ b/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs @@ -53,7 +53,7 @@ struct PointsToAnalysis<'a, 'tcx> { tcx: TyCtxt<'tcx>, /// This will be used in the future to resolve function pointer and vtable calls. Currently, we /// can resolve call graph edges just by looking at the terminators and erroring if we can't - /// resolve the callee. + /// resolve the callee. call_graph: &'a CallGraph, /// This graph should contain a subset of the points-to graph reachable from function arguments. /// For the entry function it will be empty (as it supposedly does not have any parameters).