Skip to content

Add a (default) timeout feature to kani/cargo-kani #885

@tedinski

Description

@tedinski

If the solver is non-terminating, we should have a better experience than simply running forever. Now that we have a Rust implementation of kani and cargo-kani we should introduce this feature (with a default timeout that can be extended).

  • Introduce a timeout. Decide on a default. (Random initial proposal: 2 minutes. Short enough to discover it exists quickly if you're trying to do long proofs, long enough that most proof should be fine?)
  • Add an attribute (like unwind) for proof harnesses to modify this timeout.

Metadata

Metadata

Assignees

No one assigned

    Labels

    [C] Feature / EnhancementA new feature request or enhancement to an existing feature.

    Type

    No type
    No fields configured for issues without a type.

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions