stainless
stainless copied to clipboard
Report counterexamples as test cases
Can we report counterexamples as valid Scala test functions that (at least in some cases) apply to the initial source code (before the transformations).
The user can then paste these functions directly into Scala to reproduce counterexamples.
Some of the things to make this feature work include:
- [ ] add a simple wrapper that generates function signatures with the right parameters
- [ ] make sure that the output syntax we print is valid Scala
- [ ] see how we can undo the pipeline transformations that add parameters or change types