Assess requires user to pass --legacy-linker

[celinval]

I tried the code from this workspace: https://github.com/model-checking/kani/tree/main/tests/cargo-ui/ws-integ-tests

using the following command line invocation:

cargo kani assess

with Kani version: 0.13

I expected to see this happen: I expected Kani to return some useful information.

Instead, this happened: The tables are basically empty:

Results:

Analyzed 4 crates
============================================
 Unsupported feature |   Crates | Instances 
                     | impacted |    of use 
---------------------+----------+-----------
 caller_location     |        4 |         4 
============================================
======================================
 Reason for failure | Number of tests 
--------------------+-----------------
======================================
========================================
 Candidate for proof harness | Location 
-----------------------------+----------
========================================

Adding --legacy-linker argument, returns more information.

Results:

Analyzed 9 crates
No crates contained Rust features unsupported by Kani
Checking harness test_no_overflow::{closure#0}...
Checking harness test_no_overflow::{closure#0}...

VERIFICATION RESULT:
 ** 1 of 190 failed (189 undetermined)
Failed Checks: unwinding assertion loop 1
 File: "/rustlib/src/rust/library/core/src/tuple.rs", line 31, in core::tuple::<impl std::cmp::PartialEq for (u8, bool)>::eq

VERIFICATION:- FAILED
[Kani] info: Verification output shows one or more unwinding failures.
[Kani] tip: Consider increasing the unwinding value or disabling `--unwinding-assertions`.
Verification Time: 0.18894474s


VERIFICATION RESULT:
 ** 1 of 190 failed (189 undetermined)
Failed Checks: unwinding assertion loop 1
 File: "rustlib/src/rust/library/core/src/tuple.rs", line 31, in core::tuple::<impl std::cmp::PartialEq for (u8, bool)>::eq

VERIFICATION:- FAILED
[Kani] info: Verification output shows one or more unwinding failures.
[Kani] tip: Consider increasing the unwinding value or disabling `--unwinding-assertions`.
Verification Time: 0.1891987s

======================================
 Reason for failure | Number of tests 
--------------------+-----------------
 unwind             |               2 
======================================
========================================
 Candidate for proof harness | Location 
-----------------------------+----------
========================================

The issue is due to the usage of the MIR Linker which by default performs reachability starting from a harnesses. The assess feature should be using the pub_fns reachability option described here.