You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
{{ message }}
This repository has been archived by the owner on Jul 31, 2023. It is now read-only.
The right way to support #[test] in a formal verification tool is almost certainly to implement it as part of rustc because that is how it is supported for testing.
Instead, we jump through a number of hoops to
make a list of all the tests
find the mangled names of tests
invoke each test individually
find whether a test #[should_panic]
run N copies of the verifier in parallel
This allows us to write tests that work for both dynamic verification (testing / fuzzing) and static verification (symbolic execution, model checking, ...) but the result is that scripts/cargo-verify is a collection of hacks to do the above.
The current approach makes it possible to experiment with the interface and understand the issues - but, in the long run, some changes to rustc will probably be required.
The text was updated successfully, but these errors were encountered:
The right way to support #[test] in a formal verification tool is almost certainly to implement it as part of rustc because that is how it is supported for testing.
Instead, we jump through a number of hoops to
This allows us to write tests that work for both dynamic verification (testing / fuzzing) and static verification (symbolic execution, model checking, ...) but the result is that
scripts/cargo-verify
is a collection of hacks to do the above.The current approach makes it possible to experiment with the interface and understand the issues - but, in the long run, some changes to rustc will probably be required.
The text was updated successfully, but these errors were encountered: