A RetroSearch Logo

Home - News ( United States | United Kingdom | Italy | Germany ) - Football scores

Search Query:

Showing content from https://model-checking.github.io/kani/dev-documentation.html below:

Developer documentation - The Kani Rust Verifier

Developer documentation - The Kani Rust Verifier
  1. 1. Getting started
    1. 1.1. Installation
      1. 1.1.1. Building from source
      2. 1.1.2. GitHub CI Action
    2. 1.2. Using Kani
    3. 1.3. Verification results
  2. 2. Crates Documentation
  3. 3. Tutorial
    1. 3.1. First steps
    2. 3.2. Failures that Kani can spot
    3. 3.3. Loop unwinding
    4. 3.4. Nondeterministic variables
  4. 4. Reference
    1. 4.1. Arbitrary Trait
    2. 4.2. Attributes
    3. 4.3. Bounded Non-deterministic variables
    4. 4.4. List Kani Metadata
    5. 4.5. Experimental features
      1. 4.5.1. Automatic Harness Generation
      2. 4.5.2. Coverage
      3. 4.5.3. Stubbing
      4. 4.5.4. Contracts
      5. 4.5.5. Loop Contracts
      6. 4.5.6. Concrete Playback
      7. 4.5.7. Quantifiers
  5. 5. Application
    1. 5.1. Comparison with other tools
    2. 5.2. Where to start on real code
    3. 5.3. Debugging slow proofs
  6. 6. Developer documentation
    1. 6.1. Coding conventions
    2. 6.2. Working with CBMC
    3. 6.3. Working with rustc
    4. 6.4. Migrating to StableMIR
    5. 6.5. Command cheat sheets
    6. 6.6. Testing
      1. 6.6.1. Regression testing
    7. 6.7. Performance comparisons
      1. 6.7.1. benchcomp command line
      2. 6.7.2. benchcomp configuration file
      3. 6.7.3. Custom parsers
    8. 6.8. Profiling Kani
  7. 7. Limitations
    1. 7.1. Undefined behaviour
    2. 7.2. Rust feature support
      1. 7.2.1. Intrinsics
      2. 7.2.2. Unstable features
    3. 7.3. Overrides
  8. 8. FAQ
The Kani Rust Verifier Developer documentation

Kani is an open source project open to external contributions.

The easiest way to contribute is to report any issue you encounter while using the tool. If you want to contribute to its development, we recommend looking into these issues.

In this chapter, we provide documentation that might be helpful for Kani developers (including external contributors):

  1. Coding conventions.
  2. Useful command-line instructions for Kani/CBMC/Git.
  3. Development setup recommendations for working with cbmc.
  4. Development setup recommendations for working with rustc.
  5. Guide for testing in Kani.
  6. Transition to StableMIR.
  7. Profiling Kani's performance

NOTE: The developer documentation is intended for Kani developers and not users. At present, the project is under heavy development and some items discussed in this documentation may stop working without notice (e.g., commands or configurations). Therefore, we recommend users to not rely on them.


RetroSearch is an open source project built by @garambo | Open a GitHub Issue

Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo

HTML: 3.2 | Encoding: UTF-8 | Version: 0.7.4