Skip to content

Docs are misleading about default-unwind configuration #4495

@hashcatHitman

Description

@hashcatHitman

I tried this code:

[package.metadata.kani.flags]
default-unwind = 1

using the following command line invocation:

cargo kani

with Kani version: 0.66.0

I expected to see this happen:

Kani runs with the default unwind set to 1.

Instead, this happened:

I get the message:
error: Unknown key type default-unwind

And nothing else happens. This message comes from here:

https://github.com/model-checking/kani/blob/main/kani-driver/src/args_toml.rs#L151-L183

I found that this works correctly if I instead do:

[package.metadata.kani.flags]
default-unwind = "1"

I expected it to work because of the workspace example given here:
https://model-checking.github.io/kani/tutorial-loop-unwinding.html

...and the package example given here:
https://model-checking.github.io/kani/usage.html#configuration-in-cargotoml

...which both use 1 instead of "1".

Metadata

Metadata

Assignees

No one assigned

    Labels

    [C] BugThis is a bug. Something isn't working.

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions