Kani fails to detect for loop bound after upgrade to nightly-2024-03-15 #3088
Labels
[C] Bug
This is a bug. Something isn't working.
T-CBMC
Issue related to an existing CBMC issue
T-High Priority
Tag issues that have high priority
While upgrading to nightly-2024-03-15, we had to add a few
#[kani::unwind]
attributes to harnesses with for loops with simple integer ranges. We need to investigate why this is no longer the case, and hopefully improve the loop bound detection algorithm.Here is an example of a test case (tests/expected/iterator/main.rs):
using the following command line invocation:
with Kani version: #3084
I expected to see this happen: Kani should be able to automatically detect the loop bound.
Instead, this happened: Kani requires an unwind attribute.
The text was updated successfully, but these errors were encountered: