Skip to content

RFC: Output - Reduce reported checks/properties #2574

@adpaco-aws

Description

@adpaco-aws

Requested feature: Kani's output quickly gets cluttered due to the high number of checks being reported, and assumes that all properties have the same value. We need a proposal to change this. The goal is to:

  1. Reduce the number of checks presented to the user as much as possible.
  2. Keep checks that users care about.
    It isn't entirely clear how to do (2), but one can filter in checks in the user's code or checks whose status is deemed relevant despite not being in the user code.

Use case: Standard verification reports.
Link to relevant documentation (Rust reference, Nomicon, RFC): N/A

Metadata

Metadata

Assignees

No one assigned

    Labels

    T-RFCLabel RFC PRs and Issues[C] Feature / EnhancementA new feature request or enhancement to an existing feature.

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions