Comments (2)
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.
from kani.
Thank you for your feature request! We shall discuss the feature and ping this issue if we have any updates. Thanks for using Kani!
from kani.
Related Issues (20)
- Add an option to turn `requires` clauses into assertions HOT 1
- Disable Divide by 0 Checks for Floats
- Performance drastically differs across two string indexing operations HOT 1
- Build bundle jobs could test bundles before upload HOT 1
- Kani Setup Fail MacOS HOT 3
- Modifies property points to a temporary variable
- Add contract support to intrinsics
- Checking memory initialization in presence of `copy` and `copy_nonoverlapping` produces false positives
- Function Contracts: Modifies for str
- Toolchain upgrade to nightly-2024-07-18 failed
- Harness Output in Individual Files HOT 5
- Remove terse output requirement for parallel jobs HOT 2
- Toolchain upgrade to nightly-2024-07-19 failed
- The `old` construct does not respect the function requirements HOT 2
- Toolchain upgrade to nightly-2024-07-22 failed
- Contract requirement not respected HOT 1
- Add support for transitive modifies clause HOT 1
- Enable concrete playback for contracts
- question: semantics of rust HOT 3
- Missing function/file/line information in trace HOT 2
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from kani.