[WIP] Various IDE improvements and new features #1334
Draft
Conversation
This file contains 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
(this commit is not compiling however!)
… by simply creating a fake error in the case that no_verify and show_ide_info are set.
…ps, even though they introduce some new problems
…ocket. Report quantifier instantiations split by methods.
…is was cached to clients.
In general, when skipping verification, we introduced a so called fake_error to make sure the compiler does not just cache this as successful verification and then skip later verifications even if that's not intended. Same issue occured for selective verification, when verifying a single method that is "correct", this would be cached. Now we throw a fake error in this case too, to avoid this.
Prusti Assistant offers a few new features, and it checks for this version for them to be available.
fpoli
changed the title
fpoli
changed the title
Aurel300
requested changes
Mar 4, 2023
prusti-utils/src/config.rs
Outdated
Comment on lines
105
to
106
| settings.set_default("smt_qi_profile", true).unwrap(); | ||
| settings.set_default("smt_qi_profile_freq", 10000).unwrap(); |
There was a problem hiding this comment.
Will these be passed to Z3 when not using the IDE? And in such a case, will the messages not be reported to the user? If so, QI profiling should be disabled by default.
There was a problem hiding this comment.
(After looking at how they are used in the other file:) please make these be Option<_>, such that they are only passed as arguments when a value is set. The IDE can set these if they are needed.
| } | ||
| None => { | ||
| // function is a Trait (or something else?) | ||
| // are there other cases for AssocFns? |
Comment on lines
375
to
377
| // can a single generic type have the same traitbound | ||
| // more than once with different arguments? | ||
| // I would imagine yes.. may be a todo |
There was a problem hiding this comment.
Like T: Foo<i32> + Foo<u32>? Yes, this is possible.
Also add some debug statements.
In 2 places we throw fake errors to avoid caching of successes when we should not. This lead to problems with local dependencies, since they are verified too and the fake_error ended up being thrown too early. This bug is resolved now.
First of all we separated trait bounds from generic args, since for example for a function signature within an impl block, the trait bounds at the function level can still refer to the generic args defined in the impl block. Secondly, we had a problem if a generic had duplicate traitbounds, with different generics, e.g.: `T: Foo<u32> + Foo<String>`, this is now handled correctly, under the assumption that the predicates occurr in a certain order, i.e. projections come after their respective trait. So far this seems to be always the case, if it's not I don't see how this problem can be solved.
trktby
added a commit
to trktby/prusti-dev
that referenced
this pull request
Aug 12, 2024
Ported change from PR viperproject#1334
trktby
added a commit
to trktby/prusti-dev
that referenced
this pull request
Aug 12, 2024
Port basic functionality for the new prusti-server work flow according to PR viperproject#1334 .
trktby
added a commit
to trktby/prusti-dev
that referenced
this pull request
Aug 12, 2024
Querying signatures, spans of call contract collection and call finding does not work yet. PR: viperproject#1334
trktby
added a commit
to trktby/prusti-dev
that referenced
this pull request
Aug 12, 2024
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#1334
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
Changes to support various new features in prusti-assistant.
@Aurel300
@jthomme1