[Test Generation] Comprehensive Test #4406
Conversation
|
@atomb @MikaelMayer @keyboardDrummer @robin-aws Would you have a chance to take a look at this PR? It is the last thing that should be merged prior to 4.3 release before a blog post about test generation can be published. |
4.3 is a cherry-picked release, consisting of 4.2 + some PRs merged after that, so even if this PR was merged in it 4.3 might not have all the commits that you require. Also, I was hoping we could release 4.3 today since we've already been delaying it a bit, and adding new commits may slow that down. How about we try to follow 4.3 up with a 4.4 that contains all commits from master? |
|
Thank you, @keyboardDrummer. I checked and I believe all the commits I need are on the 4.3 branch already, so adding this one would really help (although I don't know what the release process is so I understand if that might not be feasible at this point) |
| @@ -141,7 +142,7 @@ public RemoveShortCircuitingRewriter(Func<MemberDecl, bool> shouldProcessPredica | |||
| return CloneForLoopStmt(forLoopStmt); | |||
| case CallStmt callStmt: | |||
| return CloneCallStmt(callStmt); | |||
| case PredicateStmt or ForallStmt or RevealStmt: // always ghost | |||
| case PredicateStmt or ForallStmt or RevealStmt: // always ghost? | |||
There was a problem hiding this comment.
Interesting question. :) Not always ghost, it turns out. At the very least, ExpectStmt extends PredicateStmt and is not ghost.
There was a problem hiding this comment.
I see... I guess for now it means that test generation won't try to cover subexpressions within a PredicateStmt or a ForallStmt but it probably makes sense to add support for that in the future.
There was a problem hiding this comment.
Yeah, and I think that's probably fine for now.
Dargones
added
run-deep-tests
| @@ -43,6 +44,8 @@ public static class InliningTranslator { | |||
| boogieProgram = MergeBoogiePrograms(boogiePrograms); | |||
| // Finally, create bodies for the Call$$ procedures that call out to Impl$$ procedures | |||
| boogieProgram = new AddImplementationsForCallsRewriter(options).VisitProgram(boogieProgram); | |||
| // Remove proof dependency ids because they lead to errors when attempting inlining | |||
There was a problem hiding this comment.
It might be better in the long run to make the process of adding ids optional. But this seems fine for now.
There was a problem hiding this comment.
I was thinking of making the AddProofDependencyId method in ProofDependencyManager virtual and then extending the class and overriding the method so that no attribute is added but I don't know if that wouldn't break anything? Then all one would have to do to disable the annotation is to set the program's proof dependency manager to a new instance of that new class.
There was a problem hiding this comment.
Ultimately, the {:id} attributes are only used when the Boogie -trackVerificationCoverage flag is enabled. I think the easy thing to do would be to have the code to add {:id} attributes check that option, and not add them if it isn't set.
This PR adds a comprehensive test for Dafny's test generation functionality that would demonstrate the majority of the relevant features. It also removes an existing test that is completely subsumed by the new one.
This PR also makes a few minor fixes that were necessary to make this test pass:
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.