--tests
flag should enable #[test]
attributes and behavior
#3163
Labels
[C] Feature / Enhancement
A new feature request or enhancement to an existing feature.
Requested feature:
When using the
--tests
flag#[test]
attributes should be recognized by Kani.By extension it would be nice if enabling the
--tests
flag would automatically execute all#[test]
functions not marked with#[ignore]
. Otherwise you'd have to execute each function manually inside the proof harness.Use case:
During security verification i.e no assertions, nondeterminants, covers, or assumptions, it is useful to let Kani run through unit tests. Attributes like
#[should_panic]
, and#[ignore]
are not recognized and#[test]
functions are not executed when the--tests
flag is set.Link to relevant documentation:
https://doc.rust-lang.org/reference/attributes/testing.html
Test case:
Use
cargo kani --tests
to execute:This will create a failure test case because the proof harness
testerino()
panicked, but ideally it should recognize the#[should_panic]
attribute and allow a panic to occur. In addition it should execute all functions with the#[tests]
flag, thus panicking atthisWillNotExecutre()
in this instance.The text was updated successfully, but these errors were encountered: