--tests flag should enable #[test] attributes and behavior

[Necromaticon]

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:

#[kani::proof]
#[test]
#[should_panic]
fn testerino(){
    panic!("aaaa");

}

#[test]
fn thisWillNotExecute(){
    panic!("I can panic and you'll never know!");
}

fn main(){}

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 at thisWillNotExecutre() in this instance.

[Necromaticon]

Due to the state explosion problem caused by executing multiple functions in series, the --tests flag would execute the #[test] functions in isolation from each other, possibly by calling separate instances of Kani which would collect all test results before outputting the test results.
Another solution might be to add a #[kani::proof] attribute in front of every #[test] attribute while parsing the attributes.

[jaisnan]

Thank you for your feature request! We shall discuss the feature and ping this issue if we have any updates. Thanks for using Kani!