New IDE support#109
Merged
Merged
Conversation
Also comment out a line that crashes when not run from the same directory. This was problematic for working with Prusti Assistant.
Ported change from PR viperproject/prusti-dev#1334
Port basic functionality for the new prusti-server work flow according to PR viperproject/prusti-dev#1334 .
Querying signatures, spans of call contract collection and call finding does not work yet. PR: viperproject/prusti-dev#1334
Defpath only verification does not work since test_entrypoint currently just puts the entire program into the request regardless of the verification tasks at hand. Update the flags in the documentation. PR: viperproject/prusti-dev#1334
Requires the viperserver backend to support these messages too.
Every body owner function that is not passed to be verified explicitly acts as though it were pure and trusted to skip the encoding of their bodies. Additionally, VERIFY_ONLY_DEFPATH now takes a vector of String instead of just a string.
`SpanOfCallContracts` now has a vector as it's `call_spans` field so only one object is created per function definition rather than one per call. `CallSpanFinder` now also collects local functions for call contract span emission. Functions that are never called need not be emitted.
A main goal here is that the vir-viper translation happens on the same thread that encodes the program in the local verification case. This should happen so the allocated arena, which is thread local, can be used. Additionally, the JVM reliant bits are a bit more hidden from the general procedure.
* Impure generics * Fixed bug due to type parameters not being encoded * Remove fractional perm * mk_bool doesn't need extra typarams
* domain fields don't need a full encoding of their type yet * type alias for do_encode_full result * parameterise TaskEncoderDependencies by the owning encoder * remove some dependency unwraps * remove 'tcx lifetime, use 'vir * check for cycles when requesting dependencies or emitting output ref * add try operators for some emit output refs
Move backtranslation to where server messages are processed. Move `EncodingInfo` to encoder crate.
- The viper program is now sent using a `GlobalRef`, so it actually compiles. - Cache usage no longer involves the `VerificationRequestProcessing` object. - The cache is now lazy, therefore only loads if the `ENABLE_CACHE` flag is set. - The `VerificationRequestProcessing` object is no longer constructed when all the requests are cache hits. The thread it holds is also not spawned as a result.
Aurel300
reviewed
Oct 27, 2025
| @@ -1,3 +1,5 @@ | |||
| use prusti_contracts::*; | |||
Owner
There was a problem hiding this comment.
Oh I guess we need this to import the extern spec for panic!? This is not great...
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
4 participants
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.
Updates to support the Prusti Assistant IDE (Prusti Assistant PR: viperproject/prusti-assistant#264)
This work includes the changes made in #57 and also:
panic!so that assertions are treated properlyNote that (2) is necessary to ensure that the Prusti Assistant tests pass. However, this change also causes seven test cases in this repository to fail: namely, there were some tests that previously passed only because they did not report errors for assertions.
Six of the seven cases failed because they involve
body_invariantwhich is not yet handled. The remaining test case is related to type-conditional spec refinement, which, I believe, is also not yet handled.