-
Notifications
You must be signed in to change notification settings - Fork 97
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Support analyzing test code #664
Labels
[C] Feature / Enhancement
A new feature request or enhancement to an existing feature.
Comments
adpaco-aws
added
the
[C] Feature / Enhancement
A new feature request or enhancement to an existing feature.
label
Nov 24, 2021
celinval
added a commit
to celinval/kani-dev
that referenced
this issue
Dec 1, 2021
This resolves model-checking#664. I added an argument to rmc and cargo rmc (--tests) to allow users to target test harnesses as their verification function.
celinval
added a commit
to celinval/kani-dev
that referenced
this issue
Dec 1, 2021
This resolves model-checking#664. I added an argument to rmc and cargo rmc (--tests) to allow users to target test harnesses as their verification function.
celinval
added a commit
to celinval/kani-dev
that referenced
this issue
Dec 1, 2021
This resolves model-checking#664. I added an argument to rmc and cargo rmc (--tests) to allow users to target test harnesses as their verification function.
4 tasks
celinval
added a commit
that referenced
this issue
Dec 1, 2021
tedinski
pushed a commit
to tedinski/rmc
that referenced
this issue
Apr 22, 2022
…ng#672) This resolves model-checking#664. I added an argument to rmc and cargo rmc (--tests) to allow users to target test harnesses as their verification function.
tedinski
pushed a commit
to tedinski/rmc
that referenced
this issue
Apr 25, 2022
…ng#672) This resolves model-checking#664. I added an argument to rmc and cargo rmc (--tests) to allow users to target test harnesses as their verification function.
tedinski
pushed a commit
to tedinski/rmc
that referenced
this issue
Apr 26, 2022
…ng#672) This resolves model-checking#664. I added an argument to rmc and cargo rmc (--tests) to allow users to target test harnesses as their verification function.
tedinski
pushed a commit
that referenced
this issue
Apr 27, 2022
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Use case: Unit tests in Rust are typically placed in a module that is guarded by
#[cfg(test)]
, and each test is annotated with#[test]
. Thermc
andcargo rmc
commands currently exclude code under#[cfg(test)]
as well as functions annotated with#[test]
, so there is no way to analyze such code with RMC.Requested feature: A new option to
cargo rmc
(e.g.--tests
) that allows it to process test code under#[cfg(test)]
and functions with the#[test]
attribute. This would be similar in spirit to clippy's--tests
option (rust-lang/rust-clippy#1436).Link to relevant documentation (Rust reference, Nomicon, RFC):
https://doc.rust-lang.org/book/ch11-03-test-organization.html#the-tests-module-and-cfgtest
https://doc.rust-lang.org/reference/attributes/testing.html#the-test-attribute
Is this a breaking change? No
The text was updated successfully, but these errors were encountered: