AutoValue unsoundness, Test Suite runner, Paths with spaces #1252
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR adds an error for a case where AutoValue was unsound namely when it was combined with other permission resources for the same field which could result in permission amounts greater than 1 (but in a way where you could still call the method erroneously without warning if you disabled smoke checks) At first I thought simply adding an implication
perm(a.f) == none ==> Perm(a.f, read$())
would fix the issue since that prevents you from getting more than write permission, however we can then no longer perform the leak check. I might try later to see if I can do something like\old(perm(a.f)) == none
in the postcondition to conditionally add the leak check when necessary, this would still mean restricting the order in which the permissions may appear. (AutoValue must come after the normal permission resource statements)Additionally this PR also adds
bin/testSuite
which you can use to run the entire testSuite or specific test cases from the command line. To run all tests simply runbin/testSuite
, to run a specific test class runbin/testSuite -s vct.test.integration.examples.AutoValueSpec
replacing the class with your test class, or to run a specific test using its name (or part of its name usebin/testSuite -s vct.test.integration.examples.AutoValueSpec combination
. (this last command runs the test added by this PR whose name contains the filenamecombination.pvl
which we can match on with-z
) Full usage details are here: https://www.scalatest.org/user_guide/using_the_runnerFinally this PR also updates the runner scripts (on linux at least) and the classpath files (on all platforms) to work when VerCors is run from a path containing spaces.