Skip to content

Implement automatic stubbing for unreachable function #2084

@celinval

Description

@celinval

Requested feature: Users should be able to easily stub code that they expect to be unreachable from a harness in order to accelerate verification.
Use case: In some cases, such as assess, Kani takes a long time compiling and analyzing code that shouldn't be reachable at runtime from a harness. For example, format panic messages.
Link to relevant documentation (Rust reference, Nomicon, RFC): https://model-checking.github.io/kani/rfc/rfcs/0002-function-stubbing.html#future-possibilities

This would include the following tasks:

  • Compiler pass to replace the function body by a call to kani::panic().
  • Auto stubbing for common targets when enabled (only for internal usage for cargo kani assess).
  • Stub attribute to generate an unreachable stub.
  • Generate a stub set for the targets identified and used in assess so they can be used by end users.

Metadata

Metadata

Assignees

Labels

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

Type

No type

Projects

Relationships

None yet

Development

No branches or pull requests

Issue actions