Skip to content

Commit 5b6700e

Browse files
authored
Remove assess subcommand (#4111)
Remove `assess` code and any mentions of it in documentation. This command has been hidden and unused for ~2 years now. Resolves #1797 Resolves #1798 Resolves #1828 Resolves #1835 Resolves #2053 Resolves #2058 Resolves #2063 Resolves #2099 Resolves #2138 Resolves #2186 Resolves #2294 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
1 parent dea03c0 commit 5b6700e

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

51 files changed

+22
-2059
lines changed

Cargo.toml

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -67,7 +67,6 @@ exclude = [
6767
"tests/cargo-ui",
6868
"tests/slow",
6969
"tests/std-checks",
70-
"tests/assess-scan-test-scaffold",
7170
"tests/script-based-pre",
7271
"tests/script-based-pre/build-cache-bin/target/new_dep",
7372
"tests/script-based-pre/build-cache-dirty/target/new_dep",

docs/src/SUMMARY.md

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -36,10 +36,8 @@
3636
- [Working with `rustc`](./rustc-hacks.md)
3737
- [Migrating to StableMIR](./stable-mir.md)
3838
- [Command cheat sheets](./cheat-sheets.md)
39-
- [cargo kani assess](./dev-assess.md)
4039
- [Testing](./testing.md)
4140
- [Regression testing](./regression-testing.md)
42-
- [(Experimental) Testing with a Large Number of Repositories](./repo-crawl.md)
4341
- [Performance comparisons](./performance-comparisons.md)
4442
- [`benchcomp` command line](./benchcomp-cli.md)
4543
- [`benchcomp` configuration file](./benchcomp-conf.md)

docs/src/dev-assess.md

Lines changed: 0 additions & 185 deletions
This file was deleted.

docs/src/repo-crawl.md

Lines changed: 0 additions & 93 deletions
This file was deleted.

docs/src/testing.md

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -15,5 +15,4 @@ two very good reasons to do it:
1515

1616
We recommend reading our section on [Regression
1717
Testing](./regression-testing.md) if you're interested in Kani
18-
development. To run kani on a large number of remotely
19-
hosted crates, please see [Repository Crawl](./repo-crawl.md).
18+
development.

kani-compiler/src/args.rs

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -28,8 +28,6 @@ pub enum ReachabilityType {
2828
None,
2929
/// Start the cross-crate reachability analysis from all public functions in the local crate.
3030
PubFns,
31-
/// Start the cross-crate reachability analysis from all *test* (i.e. `#[test]`) harnesses in the local crate.
32-
Tests,
3331
/// Start the cross-crate reachability analysis from all functions in the local crate.
3432
/// Currently, this mode is only used for automatic harness generation.
3533
AllFns,

kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -253,7 +253,7 @@ impl CodegenBackend for LlbcCodegenBackend {
253253
units.store_modifies(&modifies_instances);
254254
units.write_metadata(&queries, tcx);
255255
}
256-
ReachabilityType::Tests | ReachabilityType::AllFns => todo!(),
256+
ReachabilityType::AllFns => todo!(),
257257
ReachabilityType::None => {}
258258
ReachabilityType::PubFns => {
259259
let unit = CodegenUnit::default();

0 commit comments

Comments
 (0)